Per-table GPU recursion, end to end: one root for block 25368371 - #985
Draft
MauroToscano wants to merge 594 commits into
Draft
MauroToscano wants to merge 594 commits into
MauroToscano wants to merge 594 commits into
Conversation
…, and the program text is hash-generic already A host FRI commitment-opening proof whose every hash — Merkle leaves, tree nodes, and the Fiat-Shamir transcript — goes through RPO, verified by the machine: sponge replay, Merkle-authenticated openings, alpha-combination, two unnormalized folds, terminal check. Plus the tamper gates that make it mean something (a tampered opened row must break its Merkle path, a tampered commitment must break the transcript replay) and the cross-hasher rejection (an RPO-committed proof must not be provable under Poseidon or Test). The finding is what did NOT have to change. `programs::fri_toy_program` is emitted once and unchanged, and nothing in it is RPO-specific: it speaks only the frozen LFM_HASH socket ops, and which permutation those rows prove is HasherKind, chosen at AIR-build time. The same program text is a Test-verifier, a Poseidon-verifier and an RPO-verifier. That matters for the three-way comparison the campaign wants. The socket-native world — edsl::merkle_walk, SpongeVar, compress/leaf/transcript_step, with the host mirror in fixture.rs already parameterised by HasherKind — is a complete, tested, field-native emitter and commitment pair. It is not something this lane has to build. A third algebraic candidate joins it by supplying a permutation and a chip arm, with zero emitter work. What remains genuinely unbuilt is the PRODUCTION path: crypto/stark commits under byte-oriented keccak/blake3 with 32-byte two-cell digests, and taking a real epoch or wrap proof to RPO is where WrapDigest has to become hash-dependent. That piece is unchanged in scope; this one turned out already done.
…ation and 2.37x RPO's host speed Rescue-Prime eXtended (XHash12, eprint 2023/1045) is a round-function swap on RPO's geometry, not a redesign: same state width 12, same rate 8 and capacity 4, same four-felt digest, same MDS, and literally the same ARK1/ARK2 tables, which this module imports from rpo rather than re-deriving so the two cannot drift. The schedule is what changes — FB E FB E FB E M, where the three FB rounds are RPO's round verbatim, the three E rounds raise four lane-triples to the seventh power in the degree-3 extension field with no linear layer at all, and the final round is MDS plus constants and nothing else. That attacks precisely the term this lane measured as dominant. The inverse S-box is 60% of an RPO permutation on the box; RPX runs three inverse layers where RPO runs seven. Measured on one machine in one run (hash_ladder_throughput, which times all three candidates and BLAKE3 together so the RATIOS are machine-independent even where the absolutes are not): RPX 2503 ns against RPO 5922, a 2.37x speedup, and 41x a BLAKE3 parent against RPO's 96x. It is also narrower in the AIR: 316 value columns and 309 constraints against RPO's 436 and 429, because an E round commits two extension intermediates per triple where an FB round commits two ladders per lane, and the M round commits nothing. Measured cells per permutation, on the same census instrument as every other column: RPX 325, RPO 445, Poseidon 621. Degree stays exactly 3 in all three round kinds. The extension seventh power lowers the same way the base-field one does — commit t2 = x*x and t3 = t2*x, then write the output as (t3)^2 * x — with each extension operation stating three base-field coefficients, which is why an E round costs 36 columns rather than 12. Padding by zero survives all three kinds, so blowup 2 is untouched. The per-mode capacity prefix is now emitted once and shared by both tenants rather than restated per arm: RPO and RPX have identical socket geometry, so that prefix was the one place their AIRs could silently disagree about domain separation. PROVENANCE IS WEAKER THAN RPO'S AND THE MODULE SAYS SO. miden publishes no RPX known-answer table — its tests are structural only. So the anchors are (a) the shared constants, MDS and FB round, externally anchored through RPO's nineteen vectors, and (b) the new extension arithmetic, pinned against naive polynomial multiplication mod x^3 - x - 1 and against generic exponentiation — different algorithms for the same functions, not a second transcription. A deployment decision should treat "no published KAT" as a real cost. NOT XHash8: its extra speed comes from a partial S-box layer, and a partial layer is one of the three structural footholds this project's own break analysis identified in the 2026 Poseidon collapse. Flagged in the module header rather than adopted quietly.
…the variance was the story The ladder reported RPO at 5,922 ns where this lane's own rpo::throughput reported 4,712 for the same code on the same machine. Two numbers for one quantity is exactly the confusion the campaign's per-number labelling rule exists to prevent, so it was worth finding out which was right. Neither, quite. Monomorphising the timing helper over the concrete hasher instead of dispatching through HasherKind moved it only 5,922 to 5,647 — so the enum was not the cause. The cause is run-to-run variance: rpo::throughput itself produced 4,712, 5,685 and 6,576 across earlier runs, roughly plus or minus 20%, which is larger than the gap between two candidates would need to be to matter. Quoting 4,712 as though it were precise was reading a lucky sample. So the ladder now takes the best of five runs at 50,000 permutations each. The minimum is the standard robust estimator for a throughput microbenchmark — noise only ever adds time — and it reproduces: two consecutive runs gave an RPX/RPO ratio of 0.56 and 0.55, and Poseidon's absolute agreed to 0.04%. The correction that matters is which output is load-bearing. Absolutes on this laptop are not; RATIOS measured within one run are, because the candidates share conditions. That is why the ladder times all of them together, and it is what the box column should be scaled by rather than by a laptop absolute. It also moves the Poseidon reading: best-of-five puts it around 1.4x SLOWER than RPO, where a single sample had shown the two roughly equal.
… a hash swap as it stands Every RPO/RPX/Poseidon figure this lane has produced is a proxy: measured chip cells and measured host ns, extrapolated cells-linearly off BLAKE3's single measured full-scale prove. The obvious cheap de-risk is the fixture, which already commits end to end under any tenant — so the question is whether it can produce one genuinely measured algebraic data point. As it stands, no. The FRI fixture verifier's LFM_HASH chip is 0.4% of its 15.9M cells (RPO 56,192; RPX 40,832; Poseidon 78,720), because the program is dominated by FIXED-height lookup tables that do not scale with its workload. Swapping RPO for RPX therefore moves the total by about 0.1%, far under this laptop's own run-to-run variance of roughly 20%. That is the opposite mix from the aggregator, whose hash table is ~85% of 12.2B cells and whose fixed floor is a rounding error, and it is the number that decides how much work a fixture-based de-risk actually is. The sizing it feeds is in HASH-SWAP-DESIGN.md section F. Asserting the finding rather than only printing it, so that if the fixture is ever scaled to where a swap IS measurable, this fails and the sizing gets revisited instead of standing on a measurement nobody re-ran.
…gainst-machine (A2) The one open correctness question in the algebraic swap. A wrap program verifies a proof the host produced, so the in-VM transcript replay must re-derive exactly the challenges the host derived. Get the encoding wrong and Fiat-Shamir does not fail loudly: the walk reconstructs nothing, a difference that should have been non-zero is inverted, and the executor reports DivByZero at an address that names neither the hash nor the site. Three facts made it tractable, each checked rather than assumed. The transcript is a caller-supplied parameter — prove and verify take `&mut impl IsStarkTranscript` — so this is a new type and nothing the byte path uses is edited. IsTranscript is already felt-native where it matters: append_field_element and sample_field_element speak FieldElement, and only append_bytes and state() are byte-typed. And append_bytes has a tiny regular call surface: across the whole STARK core it takes exactly two things, 32-byte Merkle roots and 8-byte integers, and a 32-byte root under an algebraic hash IS four felts, which is exactly one SpongeVar cell. The convention: state is one cell, zero-initialised, every step one transcript- domain LFM_HASH step, identical to SpongeVar because matching it is the point. append_bytes absorbs a length cell then the payload in 32-byte cells, as DIGESTS. append_field_element absorbs the three Fp3 coefficients as one DATA cell through the leaf encoding — a different hash domain, so a program that absorbs a root cannot claim it absorbed a field element. state() serialises the four state felts canonically for grinding. sample_u64 masks rather than rejection-samples, so it consumes exactly one cell per draw: every STARK call site passes a power of two, where the incumbent's rejection threshold is zero and its loop never rejects, and a straight-line machine cannot emit a loop whose trip count depends on a sampled value. The length prefix is the injectivity argument, not decoration: without it a 32-byte root whose tail is zero and an 8-byte integer holding the same leading bytes absorb identically. There is a test for exactly that collision, with the control showing the payload cells really are the same and the prefix is the only thing separating them. The rule is uniform rather than special-cased on 32 and 8, because a conditional encoding is how a third call shape introduces a collision later. The gate is a differential: a program drives SpongeVar through the same sequence written from the CONVENTION rather than from this implementation, is proved, and its published challenges are compared against the host's — under Test, Poseidon, RPO and RPX. If the two sides ever disagree about the encoding they disagree about the challenges, and that is a failing test rather than a DivByZero. The type is parameterised by HasherKind, so all four tenants share one implementation and a fifth costs nothing here.
…nd the gate caught the integer case Scoping the commitment backends turned up a second byte-order convention about to be born. The leaf buffers the STARK serialises reach a backend through ByteConversion::write_bytes_be, which for a Goldilocks felt is canonical_u64().to_be_bytes() — big-endian. The transcript written yesterday decoded its 32-byte cells little-endian. Two rules on one path is how a root gets produced that nobody can reproduce, so the transcript moves to big-endian and there is now ONE rule for felt-to-byte everywhere on the algebraic path: the transcript, the Merkle nodes, and the leaf buffers. Unifying it immediately broke the host-against-machine differential, which is the outcome that justifies having built the gate first. The STARK core hands append_bytes LITTLE-endian integers — (idx as u64).to_le_bytes() for query indices, heights and widths — so under one big-endian rule the resulting felt is the byte-SWAP of the integer. The machine side of the test had hand-written FE::from(SMALL), which agreed with the old little-endian decode and disagrees with the new one; the gate failed at exactly the challenge that follows the integer absorb. The fix is not to special-case eight-byte inputs, which would reintroduce the conditional encoding the length prefix exists to avoid. It is to derive the machine's payload cell from the convention — bytes_to_cell(&SMALL.to_le_bytes()) — which is what the differential was supposed to do in the first place. The byte swap itself is harmless: those call sites carry compile-time constants, so an emitter materialises whatever felt the rule produces and no runtime swap exists anywhere. It only has to be derived at both ends rather than assumed, and that is now stated in the module header next to the rule.
… three type tags (A) The host commitment layer for an algebraic hash: a batched leaf backend and a FRI-layer pair backend, both Node = Commitment, generic over the permutation. RPO, RPX and the Poseidon reference are unit-struct tags carrying a HasherKind, not three code paths, which is the objective this lane is organised around — a fourth candidate costs a permutation and a const. BLAKE3's path is not edited. These are sibling types beside FieldElementVectorBackend, which is what keeps the measured BLAKE3 record safe from this work. Three facts made it small, each checked rather than assumed: IsMerkleTreeBackend::Node is bound only to PartialEq + Eq + Clone + Sync + Send, so the trait never became byte-only; StarkHash pins Node = Commitment and a four-felt Goldilocks digest is exactly 32 canonical bytes, so the node type does not fight us; and IsStreamingLeafBackend::Data is already Vec<FieldElement<F>>. Conventions, all sharing the single big-endian felt-to-byte rule established with the transcript. A parent is compress(left, right) — one permutation in the compress domain, which is zero, so under RPO a parent is literally Rpo256::merge and externally checkable. A leaf is the rate-8 OVERWRITE DUPLEX this lane priced and adopted: capacity lane 0 carries the padding flag len mod 8, lane 1 the leaf domain, and each block overwrites the eight rate lanes with no field arithmetic outside the permutation. A1 lands as a buffering leaf hasher. Every capacity-flag padding rule needs the total length before the first permutation, so an incremental sponge cannot start until the length is known; the buffer is bounded by the row width and is no worse than the hash_data(Vec) route, whereas inventing a length-free padding rule would be a cryptographic decision this lane does not get to make. Gated on the things that can silently disagree. hash_bytes must equal hash_data on the elements those bytes encode — the trait's own contract, and the one place an algebraic backend can contradict itself, since the byte route rebuilds the felts the felt route was handed; checked over base AND extension leaves, the extension being the interesting case at three felts per element. The incremental hasher must agree with hash_data under every two-way split and a three-way one, which is the property that makes a leaf re-derivable by a verifier that only ever sees the concatenation. The block count must be the census's own closed form, which is what the rate-8 invariance rests on. And a leaf over eight felts must not equal the parent of those two digests, or the domains are not separated.
…ncoding rule exactly once Grinding is the one thing StarkHash::Transcript still decides — the challenge stream is a caller-supplied parameter — and grinding is verified INSIDE the machine. Leaving BLAKE3 there would keep the 3,056-column slot-11 chip in an algebraic branch's AIR set, so a branch would measure a hybrid rather than the hash it names. AlgebraicDigest presents the digest trait stack over sponge_leaf, and RpoTranscriptHash / RpxTranscriptHash / PoseidonTranscriptHash name the three configurations. The construction is the LEAF one, and the reason is a constraint rather than a preference: the socket pins per-mode capacities from PREPROCESSED selectors, so the only capacities an emitted program can produce are the three the chip pins. A grinding-specific domain would need a fourth mode, i.e. a change to the frozen LFM_HASH tuple contract. Grinding hashes a byte string — state and nonce, forty bytes, five felts — which is data, exactly what a leaf is. SOUNDNESS.md 6.5 records the reuse as a weakening, why the machine cannot do otherwise, and why it does not bite: the verifier RECOMPUTES the digest over a preimage the protocol fixes, so no digest is ever presented and there is no substitution surface. The reviewer checklist gains the condition under which that stops holding. SOUNDNESS.md 6.4 closes an item 6.3 opened. That section said the hash migration would have to rebuild the transcript as a field-native sponge and that constant-consumption sampling was a constraint to carry into the rebuild rather than a separate migration. It was carried: CANDIDATES_PER_COORDINATE is Some(1), guaranteed rather than probabilistic, because a squeeze returns felts canonical by construction and a carved u64 cannot miss. That is stronger than BLAKE3's two and than keccak's data-dependent loop, and it means 6.3's completeness restriction does not apply to an algebraic configuration at all — stated explicitly, so 6.3's bound is not misquoted against one. And every host-machine encoding rule is now stated exactly once. Four constants were still hand-written on the machine side to match a host convention — the two length-prefix cells, the field-element cell shape, and the leaf capacity — each of which would have agreed with the rule right up until the rule moved, which is precisely what the big-endian unification did to the last one. They are replaced by exported rules both sides call: append_bytes_cells, field_element_cell, leaf_capacity, single_block_leaf_cells. leaf_capacity matters beyond the tests, because under MODE_P the capacity is program data and the duplex emitter must supply exactly that word. The grinding gate is a differential like the transcript's: the preimage is one rate block, so the machine side is a single MODE_P row whose cells all come from single_block_leaf_cells. The digest TRAIT path is gated against the inherent one too, since grinding reaches it through the trait and a wrong impl would otherwise pass.
… the emitter one arm for the family (C + B front) CommitmentHash gains Rpo256, Rpx256 and Poseidon, with tags 2, 3 and 4 in commitment_hash_tag. Adding variants does not renumber the frozen ones, so no existing root moves and nothing is re-blessed — confirmed by the registry drift tests, which pass unchanged. WrapHash gains ONE variant for the whole algebraic family, and that is the finding rather than an economy. RPO, RPX and Poseidon share it because they share everything the EMITTER cares about: state 12, rate 8, capacity 4, and a one-cell four-felt digest against the byte hashes' two-cell 32-byte one. Which permutation the emitted socket rows prove is HasherKind, chosen when the AIR set is built — an orthogonal axis. A fourth algebraic candidate therefore needs no emitter work at all. The tripwire fired exactly where the design doc predicted, at five library sites and four test ones. Three were mechanical: blocks_for takes div_ceil(RATE_FELTS), written as its own arm rather than merged with BLAKE3's so the equality stays a checked property rather than an assumption; candidates_per_coordinate takes Some(1); wrap_hash_rows reads the socket's own table. The two that resist are hash_bytes and hash_bytes_with_rev, and they resist for a reason worth stating rather than papering over: they return WrapDigest, which is TWO cells because a byte hash's digest is 32 bytes. An algebraic digest is four felts, one cell, so no value of the return type would be correct — and the "rev" half is a BYTE reversal, which is not an operation on a field element at all. They are not functions with a missing arm; they are the wrong API for this hash. So the algebraic arm panics at EMIT time with a message naming the cause, rather than returning something wrong. That is deliberate and matches this file's existing idiom — merkle_walk already asserts "one sibling per level" when the program is built. It is not reachable by proof data, only by an emitter that routes the algebraic path through the byte API, which is the bug it exists to catch. The real fix is at the call sites in transcript_replay.rs, sub_proof.rs and batched_epoch_verify.rs, which serialise felts only because the incumbent hashes are byte-oriented; the algebraic path deletes that serialisation rather than reimplementing it, and that is the remaining piece of B, gated on WrapDigest becoming shape-carrying.
…fined exit The panic on WrapHash::Algebraic's arm of hash_bytes is accepted as an interim, not as a considered permanent choice, and the code now says so where the panic is rather than only in a lane document. This repo has a standing no-production-panic policy, and an interim panic that outlives its interim becomes a permanent one. So the requirement is recorded alongside it: when WrapDigest becomes shape-carrying, the algebraic path must become UNABLE to reach a byte-digest API, and at that point this function is DELETED rather than kept as a belt. A retained defensive panic behind a type-level impossibility is exactly the dead production panic the policy exists to prevent.
…ve call sites Five sites compared a walked root against a claimed one by spelling it as two indexed calls, assert_word_eq_lanes(root[0], ..) and root[1] — which writes the digest's cell count into every one of them. assert_digest_eq_lanes loops instead, so a digest of a different width changes one function rather than five callers. sub_proof, batched_epoch_verify twice, and fri. Behaviour-preserving for a two-cell digest, and the gate says so: 483 passed and the one standing exonerated failure, identical to before. This is the first of the two mechanical patterns standing between the emitter and a one-cell algebraic digest. The other — the Merkle walk's per-level pair of selects, which becomes ONE select under a one-cell digest — needs a digest constructor and lands with the type change rather than before it. It also records what the last unknown turned out to be. RootCells looked like a representation that would have to be generalised; following its consumers shows its halves() exists to feed the BYTE transcript's append_halves, and its whole shape is a 32-byte root read the way a byte hash wants it. An algebraic root has no u32 lanes — it IS four felts, one cell — so it is absorbed by SpongeVar::absorb and compared by cell equality, and neither route needs halves. RootCells is therefore bypassed rather than generalised, the byte-world type stays untouched for the byte hashes, and the socket world already has the type the algebraic path needs in DigestVal, which edsl::merkle_walk already walks.
…aic digest is expressible WrapDigest was `[Cell; 2]` — the byte hashes' 32 bytes as two words. An algebraic digest is four field elements, ONE cell. It is now a struct carrying its own width, so the shape travels with the value instead of being written into every call site. It derefs to [Cell], so `d[0]`, `d.len()` and `d.iter()` keep working and the forty-odd sites that only carry a digest around are untouched. What changed is the handful that knew the count: the two Merkle walks, the arena-hinted sibling readers, and the byte-hash returns. ★ Both Merkle walks are now loops over the digest's cells rather than two hard-coded halves. Under a one-cell algebraic digest that is ONE select per level where a byte digest costs two — the saving this lane predicted from reading the code, now expressible rather than argued. The arena-hinted sibling readers are the interesting ones. Each read two words per sibling because a byte digest is two cells, which is `sub_proof.rs`'s `2 * merkle_depth * groups` arena budget written out longhand at four more sites. They construct through `WrapDigest::from_pair` now, so when the algebraic path lands the stride follows the width rather than a literal. The grinding seed and the transcript's squeeze buffer also take a WrapDigest rather than a fixed pair, so an algebraic seed needs no further change there. Behaviour-preserving, and the gate says so: 483 passed with the one standing exonerated failure, identical to before the change. This is scaffolding for the algebraic path, not the algebraic path — nothing yet constructs a one-cell digest, which is why nothing moved.
…t backend WrapHash::Algebraic now emits real constructions instead of routing through a byte API that has no meaning for it. A parent is one compress row — the socket primitive that already existed and was gated — and under RPO the compress domain is zero, so it is literally Rpo256::merge. A leaf is the rate-8 overwrite duplex: each block overwrites the two rate cells and carries the capacity cell from the previous permutation, which is exactly MODE_P, three cells in and three out, already in the frozen bus contract. Eight fresh felts per permutation against the socket leaf chain's four — the convention this lane priced at 25% of the aggregation program. Every constant comes from the one rule rather than being restated. The capacity is program data under MODE_P, so a second definition of it would be a root the host cannot reproduce; leaf_capacity is called, not copied. The gate is the pair the whole migration turns on: the host commits with hash_data and hash_new_parent, and the wrap program re-derives them with leaf_hash and hash_pair. If they disagree the walk reconstructs nothing and the failure surfaces as a DivByZero deep in a query walk, naming neither the hash nor the site. So it is a differential across all three tenants, at six leaf lengths chosen to cross the rate boundary in both directions, because the padding flag is the one part of the construction that is not identical on every block. It also asserts the digest really is ONE cell, which is the property the shape-carrying WrapDigest exists to make expressible. 484 passed with the one standing exonerated failure.
…c path sub_proof::emit_leaf_hash and batched_epoch_verify::emit_group_leaf_hash both built a byte stream by unpacking each Fp3 value into three lanes and writing each lane as big-endian halves. That serialisation exists only because the incumbent hashes are byte-oriented: what it encodes IS three field elements per value. The algebraic path deletes it and absorbs the felts, which is the whole shape of this migration — not a reimplementation of the byte path in field arithmetic, but the removal of a step that was only ever there for bytes. sub_proof already had a felt-native route for base-field groups, so only the extension branch needed it; batched_epoch_verify needed both, since a mixed group carries base and extension matrices together. The correctness of this rests on the host and the machine decomposing an extension element the same way, and that is now gated rather than argued. ByteConversion for an Fp3 element writes components 0, 1, 2 in order, each canonical big-endian, so the host's felts are [c0, c1, c2] — and the machine's unpack(cell)[..3] is the same three lanes in the same order. The emitter differential now covers extension leaves at one, two, three and five elements alongside the base-field ones, against the host backend, for all three tenants. Two of the three call sites done. The third, transcript_replay, is materially larger and is reported separately: it is built on a byte-SEGMENT model — SegPiece::Const(Vec<u8>), SegPiece::Halves, and a packer that chunks bytes into u32 halves — where the algebraic transcript is a compress chain absorbing cells. That is a parallel replay rather than a branch, and the pieces for it already exist and are gated from A2.
…c arm, and the append call boundary becomes structural The third and last of the leaf call sites. TranscriptReplay now has an algebraic arm that drives edsl::SpongeVar instead of packing a keccak segment, gated host-against-machine under all four algebraic tenants. The finding that made this more than a mapping is that the append CALL BOUNDARY is load-bearing, and it was invisible. A keccak or BLAKE3 transcript absorbs into one flat segment, so two appends and one append of their concatenation are the same digest — the packer relies on that to concatenate constant runs before chunking. An algebraic transcript prefixes every call with its length, so the same two appends are a different transcript. The pending list is therefore now one entry per host append_bytes call, and the byte arm flattens it into the packer pieces it always used, discarding boundaries the byte stream does not have. The byte arm is behaviour-identical. It caught two live instances immediately. append_digest was two appends for one host call. append_ext routed through three append_felts, where the algebraic host is calling a different method entirely — append_field_element, one data cell — rather than the same one over different bytes. The gate localised the second one on its own: the first challenge agreed and the second did not, which names the two absorbs between them without a print. A Merkle root costs nothing on this arm. The host absorbs it with append_bytes(root), whose payload cell is bytes_to_cell(root), and an algebraic backend serialises its digest as four canonical big-endian felts — so that call recovers exactly the digest cell the backend started from and the serialisation cancels. What still pays for a byte encoding is the genuinely byte-shaped data: a keccak ELF digest, a public_output run, a big-endian nonce. The cheaper route for those is recorded in the code rather than taken, with the reason. Two collapses make the arm cheaper rather than merely different: sample_ext is one squeeze where the byte transcript carves three candidates, which also retires the whole candidate apparatus for that draw, and append_ext is one absorb where the byte arm paid three big-endian renderings. with_seed states the seeding convention once — the seed is the transcript's first append_bytes call and nothing more special — so the two sides cannot disagree about whether it is inside the transcript or beside it.
… host call, not one run Two live instances of the boundary class the previous commit made structural. Both were correct under a byte transcript and would have been wrong under an algebraic one, which is exactly why neither showed up before: a keccak transcript concatenates and cannot see an append boundary, so a single run and the sequence it concatenates are the same digest, and the packer chunks them identically either way. absorb_epoch_statement collapsed the counts, the page total, the FRI byte and the range list into one constant run where absorb_statement_with_digest makes twenty-odd separate append_bytes calls. emit_shape_histogram collapsed absorb_shape_histogram's 1 + 2n calls into one. Under length prefixing each would absorb one long field where the host absorbed many short ones, and every challenge downstream would diverge. The byte arm is unmoved and that is checked rather than argued: the emitted halves are identical because the packer concatenates consecutive constant runs before chunking, so the program text does not change, and the registry drift tests — which fold the instruction stream into every program_id — pass unchanged.
…hes on the algebraic arm The last of the legs that reached a byte-stream hash from the algebraic path. is_valid_nonce is H(H(PREFIX || seed || factor) || nonce), and under AlgebraicDigest the host reaches those bytes through felts_from_bytes, which reads eight-byte big-endian groups. Both preimages are therefore already felts: the seed is the transcript state's four canonical felts, the inner digest is four canonical felts, and the nonce's eight big-endian bytes are the nonce. So the leg is two permutations and one bit decomposition where the byte arm builds two byte strings and hashes them, and the inner digest cell needs no repacking at all because its four lanes ARE the outer preimage's first four felts. Every constant comes from the host's own rules rather than being restated — the byte-to-felt grouping from felts_from_bytes, the rate and capacity split and the padding flag from single_block_leaf_cells — and the asserts pin the lane PLACEMENT those rules imply, so the packs are the rule rather than a copy of it. emit_grinding_check now takes the nonce as a felt rather than as its two big-endian halves, because the halves are the byte hash's rendering of it and the algebraic arm needs the value. The transcript absorb at both call sites becomes append_felt, which is byte-for-byte what those sites already built by hand on the byte arm and is the free lane-0 cell on the algebraic one. The gate grinds a real nonce host-side under RPO, RPX and Poseidon and requires the emitted leg to prove on it and to be unprovable on nonce + 1. The negative control is what makes it mean anything: a leg that asserted nothing would pass the positive half. It checks the LEG rather than the digest, which is a different claim — the leg builds two preimages, and getting either one's felt layout wrong gives a digest that is individually well-formed and collectively wrong.
…ebraic panic is deleted algebraic_byte_hash_unreachable was recorded as an interim whose exit condition was that the algebraic path becomes unable to reach a byte-digest API, and that the panic is then deleted rather than kept as a belt behind a type-level impossibility — a retained defensive panic being exactly the dead production panic the no-production-panic policy exists to prevent. This is that exit. ByteWrapHash carries hash_bytes and hash_bytes_with_rev, and WrapHash::byte_hash() -> Option<ByteWrapHash> is the only way to obtain one. An algebraic configuration cannot name the byte-stream constructions, so there is nothing left to defend against, and every call site's None arm is that site's algebraic implementation — the exhaustiveness that used to be an assertion is now the control flow. The Merkle constructions deliberately do not split. leaf_hash, hash_pair and merkle_walk are shape-generic already: they take and return WrapDigest, which carries its own width. Only the byte-stream entries have no algebraic meaning, and splitting the rest would trade a real distinction for a wider one. wrap_hash_bytes now takes the hash rather than reading the builder's, and the asymmetry with the other free functions here is the signal: the rest are total over every configuration and this one is not, so the parameter is the proof that the algebraic case was handled upstream. blake3_sponge_program_source names ByteWrapHash::Blake3 outright, which a program that is about a hash should do anyway.
…so an algebraic hash becomes selectable rather than merely implemented RpoStarkHash, RpxStarkHash and PoseidonStarkHash: one StarkHash each, pairing the two Merkle families with the Fiat-Shamir configuration they belong to and the CommitmentHash they all are. IsStarkProver and IsStarkVerifier are already generic over this parameter, so naming one of these at a call site is the whole flip — there is no global to re-point and nothing in crypto/stark moves. They live in prover rather than in crypto/stark/src/config.rs because crypto/stark does not depend on prover, so a configuration built from these backends cannot be written there; the impl is legal here because the type is local. Moving the backends and the three permutations down into crypto so the workspace-wide DefaultStarkHash alias could name them would re-point a default the whole workspace shares in order to reach three branches, and would put every blessed BLAKE3 artifact's enforcement in the blast radius of a comparison experiment. The pin belongs at the layer the block path lives in. Batched and Pair are the same hash by construction rather than by convention — both are the generic algebraic backends at the same H — so a configuration mixing two permutations is unspellable rather than something to assert against. One obstacle, solved without widening anything the workspace shares. StarkHash's associated types carry FieldElement<F>: AsBytes + Sync + Send and no more, while the algebraic backends additionally required ByteConversion, so they could not be a StarkHash::Batched at all. AsBytes and ByteConversion are the same bytes for both Goldilocks fields — the base field's as_bytes IS to_bytes_be, and the degree-3 impl streams by calling write_bytes_be — so element_felts now takes the identical bytes through the weaker bound. The tests deliberately keep building their expected felts with write_bytes_be, which makes that identity a differential rather than a claim. Not available under cuda, and that is the KeccakTreeBackend marker working rather than a gap: a cuda build drives the commit phase on device with the keccak kernels, so StarkHash there requires the backends to BE keccak, and an algebraic configuration is inexpressible rather than merely unused. That is what stops a build producing keccak trees labelled RPO. Blake3StarkHash is gated the same way and for the same reason. The inhabitation check instantiates all three at both fields the prover actually commits over, because an impl that type-checks in isolation can still be unusable at the instantiation that matters.
…n change it without moving the workspace default hash_pin is now the one place a build says which hash the BLOCK path proves under. A hash-comparison branch changes three items in that file and nothing else in the workspace, so crypto/stark's DefaultStarkHash, its COMMITMENT_HASH const assertion and every blessed BLAKE3 artifact keep their enforcement while a sibling branch proves under RPO. This is expressible because IsStarkProver is generic over the configuration and prover was already naming DefaultStarkHash explicitly at each of its prove and verify call sites — those are type parameters, not a global, and collecting them turns a property spread over six files into a property of one. The pin is TWO things, and the second is easy to miss. StarkHash::Transcript names a TranscriptHash — a digest configuration, which is what grinding computes over — while the Fiat-Shamir transcript OBJECT is built by the caller, so the type system does not force the two to match. For the byte hashes they coincide: the object IS DefaultTranscript<E, H::Transcript>. For an algebraic hash they do not, because AlgebraicTranscript is a compress chain over cells rather than a byte sponge over AlgebraicDigest. A branch that pinned only the type alias would commit under RPO while sponging Fiat-Shamir through bytes — self-consistent between prover and verifier, and therefore silent. That is the half-flip DefaultStarkTranscript's own doc warns about, and pinning the constructor is why it cannot happen here. The commit helpers move with it, and registry.rs's own recorded condition is what licenses that. It said the helpers were hard-wired to the default aliases by design, so the global const was the truthful name for their output, and that if they were ever threaded the read would move with them. They are threaded now: commit_lde_columns, PrepRoundBuilder, proof_arena's MainBackend, and the three preprocessed roots in tables/ all commit under the pin, and lfm_program_id names it. The two axes still move together; the axis they follow is the pin rather than the alias. Still deliberately not an H parameter on build_artifacts_with_hasher — a build-wide pin keeps one answer per build, where a parameter would reintroduce artifacts naming an H the helpers did not use. The three preprocessed roots were the subtle ones. They are absorbed by the block path's verifier, so a root left on the alias would be the one BLAKE3 artifact inside an RPO proof, and it would fail as a root nothing reconstructs — naming neither the hash nor the site.
…hash pin, found by flipping it The pin was set to RpoStarkHash and AlgebraicTranscript, built, and run against this crate's own prove and verify tests. Everything here is what that trial found; none of it is visible on a build that only ever pins BLAKE3. stark::prover::Prover is GenericProver at DefaultStarkHash, so it is BLAKE3-fixed whatever H a call site passes alongside it. The IsStarkProver impl itself is fully generic, so the fix is a BlockProver and BlockVerifier alias at the pin rather than anything in crypto/stark. It failed loudly as a type error rather than silently proving under the wrong hash, which is the good outcome and worth recording as such. compute_expected_commit_bus_balance_view took a concrete DefaultStarkTranscript. On an algebraic branch the transcript is a different TYPE, not the same type over a different digest, so it takes any IsTranscript now. proof_arena reached hash_data_from_slices through the byte backend's INHERENT method. The unqualified call resolves to that method and then fails to exist under any other pin, so it is named through IsStreamingLeafBackend — the form every backend has. With those three fixed the flip compiles and runs, and fails exactly where it should: PrecomputedCommitmentMismatch. bitwise, keccak_rc and page each return a blessed static constant from preprocessed_commitment rather than recomputing, so under a new pin the prover recomputes an RPO root, compares it against a BLAKE3 one, and refuses. That means a pin change needs TWO governed regenerations, not one — compute_lfm_registry for the program ids and compute_static_commitments for the preprocessed roots — and the module header now says so with the failure it produces, because the second was not in the plan and is not optional.
…ic root can be one cell instead of two Three types wrote the byte digest's cell COUNT into themselves — RootCells.lanes, LayerCommitment.root_lanes, GroupCommitment.root_lanes as [[Felt; 4]; 2], and proof_arena::commitment_words returning [LfmWord; 2]. An algebraic root is one cell of four felts, so each was a hard stop rather than a slower path: RootCells indexed digest[1], which is out of bounds on a one-cell digest, and the arena reader consumed two words where the writer would produce one. The comparison layer needed nothing. edsl::assert_digest_eq_lanes already zips a digest against these lanes and asserts the widths agree, which is what it was written for when WrapDigest became shape-carrying, so it works at either width once the lanes stop being fixed at two. commitment_words' own doc already named the target layout as the thing it was not — "This is NOT pack_digest's layout, that one packs four FULL felts" — and that is exactly what an algebraic root is. The conversion goes through the backend's own commitment_to_digest rather than a second spelling of it. The nine transcript absorbs collapse into RootCells::absorb. halves() is gone as a public method deliberately: it spelled "a root is eight u32 halves" into every caller, and those halves are FULL FELTS on an algebraic hash, so a byte-stream absorb of them would be silently wrong. lanes_flat replaces it for the hash-pinned instruments, documented as meaningful only where the caller already knows which arm it holds. One invariant now has two readers and deserves a reviewer's eye: the arena writer's word count and the machine reader's must agree or every root in the arena is off by a word. They agree because both are functions of the configuration's WrapDigest width and neither restates it. No-op on BLAKE3 by test: full lfm:: suite unchanged at 487 passed, and the six registry drift tests — which fold the instruction stream into every program_id — pass unchanged.
… width, in one place instead of eleven Eleven sites wrote a root's word count as the literal 2 — arena declarations, read cursors, and the host-side word counts the leg asserts its arenas against. Three of them carried a comment saying, in the code, "Two arena words per sibling IS the digest's width. When the algebraic path lands this stride follows the width rather than the literal." This is that landing. They now go through edsl::digest_words for the machine side, which reads the builder's configuration, and proof_arena::words_per_root for the host side, which reads the production one. The two must agree or every root in the arena is off by a word; they do because both are functions of the configuration's digest width and neither restates it. The rest is a consequence: edsl::hint_digest reads one commitment out of an arena at whatever stride that is, so the three cursor loops stop spelling a pair of hint_words and a += 2. Found by running the algebraic wrap leg, which failed at each of these in turn — the digest-width assertion, then the opening arena's declared size, then the FRI arena's, then an ArenaLenMismatch, then three ArenaOutOfBounds. No-op on BLAKE3, where digest_words is 2: the full lfm:: suite is unchanged and the six registry drift tests, which fold the instruction stream into every program_id, pass unchanged.
…the composition, not the primitive The leaf and parent primitives were gated; their COMPOSITION over a height group's several matrices was not, and that is a different claim. A leaf hash correct for one matrix can still be fed the wrong felts, in the wrong order, or with the wrong padding flag, once several are concatenated. The expectation is the host's own backend rather than a reimplementation of it: hash_data over the concatenated values IS mmcs.rs's hash_group_openings — for each matrix, all evaluations then all evaluations_sym, flat, one hash — so a misunderstanding shared by both sides cannot make this pass. The shapes vary on the axes that could hide a break rather than on one convenient instance: several matrices of differing widths, the felt count straddling the rate boundary in both directions and landing on it exactly, and the single-matrix degenerate case. The padding flag is len mod 8, so the boundary is where a duplex break would hide. Groups are homogeneous in field, matching production, where a round is base or extension and the round is what groups by height. Green under RPO, RPX and Poseidon across all ten shapes, so the mixed group leaf is not the wrap leg's DivByZero. That is the point of writing it: naming what the disagreement is NOT is how the last several were found.
…ification, at both padding boundaries The emitter gate drives a 32-byte root through cells_from_halves_be, so the aligned whole-half path was covered. The statement leg produces two shapes it never reaches, and both come from real data rather than from a corner case anyone chose: a byte length that is not a multiple of four, because public_output is collected one byte per COMMIT and its length is whatever the workload produced, and a length that is not a multiple of 32, so the final payload cell is short and bytes_to_cell reads a zero-filled buffer left-justified. Those two paddings are independent and both are silent when wrong. The statement is absorbed first, so one wrong felt diverges every challenge downstream and surfaces as a DivByZero deep in a query walk, naming neither the encoding nor the site. Eleven lengths, chosen to hit each boundary exactly and miss it in both directions, against AlgebraicTranscript itself rather than a second copy of the rule. Green under all four tenants, so the regrouping is not the wrap leg's DivByZero either.
…rd — the fifth instance of the append boundary absorb_lfm_statement appends each public word as FIVE calls: the index, then each of the four lanes as its own canonical u64. emit_lfm_statement absorbed the index and then all eight halves in a single call — two calls where the host made five. Identical bytes, so a byte transcript cannot tell the difference and the drift tests pass either way. Under length prefixing they are different transcripts, and the LFM statement is the first thing a wrap leg absorbs, so the divergence reaches every challenge in the leg. That is the fifth live instance of the class and the first one found in the LFM statement rather than the epoch one. The statement gate lands with it, and it is the reason the fix was findable: it drives statement::absorb_statement_with_digest and absorb_epoch_statement from the same shape data and compares the sampled challenge, so a coalesced or miscounted call fails loudly instead of surviving as bytes that happen to concatenate the same way. The epoch statement passes it — that sequence, fixed earlier by reading, was right — which is what narrowed the search to the LFM one. Byte arm unmoved: the six registry drift tests, which fold the instruction stream into every program_id, pass unchanged.
…nd a spine diagnostic that says which challenge diverged decode and register built their preprocessed commitments through stark's default aliases rather than the block path's pin. Both are roots the prover recomputes and compares against, so under a different pin they failed at prove time with PrecomputedCommitmentMismatch — loud, and naming the cause, which is how they were found. They join bitwise, keccak_rc and page on lfm::commit's helper. The epoch and aggregator test harnesses built their Fiat-Shamir transcript as DefaultStarkTranscript while proving through the pinned prover. That is the half-flip hash_pin::block_transcript exists to prevent, arriving through the test side: proving under one hash while sponging challenges through another, self-consistent and therefore silent. They go through the pin now. RootCells::byte_halves is the inverse of the regrouping gadget, and it exists because program_id is DELIBERATELY keccak over bytes whatever the configuration commits under — its host counterpart names PlatformKeccak256 explicitly, since it identifies a program to consumers rather than being part of the commitment layer. So one fold still wants bytes after everything around it became felts. On a byte hash the lanes already are those halves; on an algebraic one each felt renders as its eight big-endian bytes, which is the serialisation digest_to_commitment performs host-side. Not lanes_flat, which yields FELTS there and would hash four values as if they were eight. The remaining root arena declarations follow words_per_root — the ones that bind a root, not a_pc_start, which is a u64 carried as two halves and must stay two. And the spine diagnostic: the same leg with the openings omitted, so nothing authenticates and nothing can divide by zero. The full leg's failure mode when an absorb diverges is DivByZero deep in a walk naming neither the absorb nor the site; this build turns that into the first challenge that disagrees, which names where to look. Keep it even while the leg passes — it is the difference between a transcript bug that reports itself and one that has to be bisected. Byte arm unmoved: the six registry drift tests pass unchanged.
…rather than inside it The batched epoch spine under an algebraic pin executes cleanly and then disagrees about the shared LogUp z. That challenge is drawn after exactly two things — the statement absorb, which its own gate covers, and Phase A — so this covers the other one. Beside the spine, not instrumented inside it: publishing the machine's intermediate transcript state to bisect was tried and introduced a DivByZero of its own, because the extra public word perturbs the program under test. A differential that stands alone cannot do that. The host side is driven through production's own absorb_shape_histogram rather than a restatement of it, then the roots in the verifier's order: the histogram, every preprocessed root from the AIR set, the carved root when the shape has one, the single batched main root, then the pair. Roots are synthetic because what is under test is the SEQUENCE and the encoding, and controlling both sides is what makes a disagreement attributable to one of them. Green under all four tenants. So Phase A's sequence and encoding are not the spine's divergence either, which leaves the DATA the spine feeds — the roots it reads from the arena and the AIR set — rather than how it absorbs them.
…e, and it failed on the byte arm Added earlier in the belief it would turn the wrap leg's DivByZero into a named challenge divergence. It does not: the openings-less build publishes no public words at all, so the test indexed an empty slice and failed on BLAKE3. The diagnosis it was credited with came from the_batched_epoch_challenge_spine_matches_production, which does publish its challenges and did name the shared LogUp z. Removed rather than repaired: the epoch spine test already covers the need, and a second one that has to be taught to publish adds a maintenance surface without adding a check. A test that fails on the shared base is worse than no test, particularly on a base four branches are cut from.
…uctions in the Phase A gate hash_pin named the commitment hash and the transcript; it did not name the LFM_HASH socket permutation the machine's own Instr::Hash rows compute. That is a third axis and it is orthogonal to the other two — the socket hasher is passed per call to execute and lfm_prove_with_hasher, and nothing in the type system makes the two agree. It went unpinned because a byte hash makes it irrelevant: the emitter's Merkle work goes through ByteWrapHash::hash_bytes, which lowers to the dedicated KECCAK and LFM_BLAKE3 chips and emits no Instr::Hash at all, so the hasher handed to execute is never consulted and passing TestPermutation is free and correct. The algebraic arm goes through compress and permute, which ARE Instr::Hash, executed by whatever is passed. The same distinction the byte hash made irrelevant, needed back — the third instance of that, after the append call boundary and the transcript constructor. Thirty-eight execute and prove sites across the three harnesses now name BLOCK_HASHER rather than a literal, so a test cannot half-flip while production stays correct. On this branch it is HasherKind::Test, which is exactly what those sites passed before. The Phase A gate drove preprocessed roots through RootCells::constant only — the Cells arm — while production reaches them two ways: program text through append_const_bytes as literal bytes, proof-carried cells through RootCells. It now drives both against the same host call. Under a byte hash they are the same 32 bytes; under an algebraic one they are a byte cellification and a digest cell, which is only the same thing if bytes_to_cell and commitment_to_digest agree. Green under all four tenants, so they do — and the earlier version of that gate claimed to cover the phase while touching one of its two arms.
…e worker and two The level-2 A/B exposed it: the same node's `prove` field read 4.8 and 4.1 serially and 5.0 and 7.1 at two siblings. None of that is work. A queued worker's wait for the card lands inside whatever phase was running when it asked, so `prove` absorbed it and the two arms stopped being comparable — which is the one thing a scheduling A/B needs them to be. `multi_prove` is now reported NET of the wait, and the wait is its own field on both lines. The node's TIMING line says explicitly that the wait is CONTAINED in `build_artifacts` and `prove` rather than additional to them, and splits it between the two, because those are wall times and a reader cannot otherwise tell which phase queued. That also closes the level's accounting. At K workers a level spends K × wall worker-seconds, of which the permit's `held` is the card, the per-node waits are the queue, and the remainder is host work. Level 2 measured `held 13.3s of 19.5s` with no way to price the other 25.7 worker-seconds; now there is one. The counter is MONOTONE and per-thread, read-only, never cleared. A take-and-clear counter couples every reader to every other one: whoever samples first silently steals the wait from whoever samples next. Callers bracket the span they care about and subtract, which composes — the driver does it around the artifact build and `lfm_prove_with_residency` does it around `multi_prove`. Both new clauses are ABSENT when the wait is zero, so a serial line stays byte-identical to every one already in the campaign's logs and the arms diff on their numbers rather than on their shape. Gated on the waiting thread itself: the blocked worker's self-reported wait must be at least half the hold and must agree with the wait observed from outside to within 50 ms. And the prove-split coverage floor now counts the wait, without which it would start failing in the one regime it most needs to hold in.
… order The level-2 ABBA caught it: the second lever arm printed L2N1 before L2N0, because a worker prints when it FINISHES. A raw diff of those lines therefore files a scheduling order as a byte difference, which is a false red on the one gate that exists to rule byte differences in or out. Sorting both sides is a correct remedy and remains sound — each line begins with its own node label, so a permuted tree still sorts differently and the check keeps its teeth. But it is a step a reader has to remember, and the reader who forgets reports a failure that did not happen. The join already holds every child in index order and `RealChild` carries its own artifacts, so printing there costs nothing and needs no procedure. The line also now carries cells and instructions, so it subsumes the census for this purpose and ONE grep is the whole gate rather than two that must be sorted and compared separately. ⚠ For logs already produced at `7a8f3e96`, sort both sides before diffing — that commit prints on the worker.
…nstrumented ⛔ NOT PUSHED until the e2e pair reports. Written so the numbers can be read against a design rather than the other way round. Nineteen epoch wraps now prove `LFM_TREE_SIBLINGS_L0` at a time, through the same card permit and the same index-ordered join as the interior. A SECOND KNOB, defaulting to 1 rather than to the interior's value. The falsifiers are different: the interior's binding constraint is the card, level 0's is the HOST PEAK, and one knob would let a safe interior setting arm the risky level — discovered by exhausting 57.53 GiB two hundred seconds in. They are also different machines: measured, a level-1 node is device 3.80 s against host 3.86, one to one, while a wrap is 2.85 against 7.90, one to 2.8. The count that saturates one starves the other. And unset, level 0 runs exactly as it did, so every existing e2e number stays comparable. Deliberately not a list on the existing knob: that spelling makes the common case need punctuation and lets a typo arm level 0 silently, which is the one thing this must never do. THREE LINES THAT DID NOT EXIST, and the first is why this commit is more than a scheduler. Per-wrap host peak. The count is chosen on what a second live wrap transient costs, and nothing measured it. The interior prints a per-node peak and that is how its retention per node was read; level 0 printed none, so the figure could only be scaled from a node, which is a different machine. The serial arm now measures it directly. The level's own host peak, which is the figure the 52 GiB stop is about — the per-wrap peaks become process-wide readings inside overlapping windows the moment wraps run together, and the line says so on itself. A per-wrap IDENTITY line at the join, the same shape the interior carries, so one grep covers the whole tree and the wraps get the same byte gate the nodes have. The permit's own line prints for level 0 too, so `max holders 1` is asserted there and `held` against the level wall says whether the card or the host was the wall — which is the evidence for whether a higher count would buy anything.
…te flag out of the memory cell Two allocation changes inside `execute`. Neither changes what is executed, recorded or proved: the bytes are identical. RECORDS ARE SIZED, NOT GROWN. Ten record vectors were built by `push` doubling while the compiler already held every one of their final lengths. `ColumnGroup::real_rows` is not an upper bound on a record count — it IS the count: pass 2 opens exactly one column-group row per instruction and this executor pushes exactly one record per instruction of the same chip. The trace fill already depends on that identity, filling rows `0..real_rows` by indexing the record vector, so a short vector is a panic there today. Sizing from it is therefore a use of an invariant the code already relies on, not a new assumption. Doubling instead re-allocated and copied every vector ~log2(rows) times per proof — a few hundred MB of memcpy and ~20 large reallocations, on each concurrent worker at once. THE OCCUPANCY FLAG LEAVES THE CELL. `LfmWord` is `[F; 4]` = 32 bytes and a Goldilocks felt has no niche, so `Option<LfmWord>` is 40: the flag cost 8 bytes per address AND pushed the stride off the cache line, so a cell spanned two lines at half of all addresses. It becomes one bit per address in a separate array — `num_addrs / 8` bytes, which stays cache-resident where the value array cannot — and the value array keeps a 32-byte stride and shrinks 20%. THE WRITE-ONCE CHECKS ARE UNCHANGED, AND NOW EACH HAS A TEST. A second write is still `DoubleWrite`, a read of an unwritten address is still `ReadBeforeWrite`, and an address past the end still reports differently in the two directions. `DoubleWrite` already had a test; `ReadBeforeWrite` had none from the executor — only from the validator — and that gap matters more after this change than before it. The value array is zero-filled, so the bit is now the ONLY thing separating "never written" from "written zero", where `Option` carried that distinction inside the cell: dropping the check would hand out zeros instead of failing. Both halves are asserted — a written zero reads back as a value, an unwritten address does not — together with both out-of-range directions. Two more pins, because both of these are claims about layout that a later edit could quietly cost. `the_memory_cell_divides_the_cache_line` fixes the 32-byte stride the argument above rests on. `the_records_are_sized_from_the_census` asserts `capacity == real_rows` per chip on a fixture whose row counts are deliberately not powers of two, so push doubling overshoots and says so; the same identity is asserted for every program under `debug_assert` at the end of `execute`, where the emitter and the executor arm are written.
…hase `lfm_prove_with_residency` held the whole `LfmExecution` — the final write-once memory and all ten record vectors — to the end of its scope, so both stayed live across the fill AND the whole `multi_prove` card phase. On a wrap that is a few hundred MB of memory plus a few hundred MB of records kept for nothing, on every concurrent sibling at once. `memory` has no consumer on the proving path at all: it is a diagnostic surface the tests read. `records` are consumed by the fill and dead the moment it returns — the traces it produced are the live set from there on. So `execute`'s result is destructured, `memory` dropped straight after it, and `records` dropped straight after the fill. TIME-NEUTRAL BY CONSTRUCTION. Both drops sit AFTER the `elapsed()` read of the phase they follow, so `execute` and `fill` keep measuring exactly what they measured before and stay comparable across this change; only the wall absorbs the free, which is a handful of `munmap`s. The value is not the clock. It is the host PEAK, which is the quantity that fenced a third concurrent interior sibling: interior 3 measured 54.36 GiB on the 120 GiB host, past the 52 GiB stop on the 57.5 GiB one. This is a straight subtraction from every live proof's footprint through the phase where the peak is taken.
…g a parallel executor Lane E measured the LFM executor at ~83% software RPX permutation: 644,250 of a wrap's 5,388,182 instructions are `Instr::Hash`, each of which runs exactly one permutation (every mode falls through `permute_two_cells` to `permute`), and a permutation costs 2,356 ns on Zen 5. That makes "run the permutations in parallel" the largest remaining host lever. The case for it rested on reading the emitters — the per-table legs are transcript-forked, the per-query blocks are contiguous — which is an argument, not a number. This measures it instead. One forward pass carries, per instruction, the length of the longest chain of DEPENDENT hash instructions ending there. Grouping the hashes by that number gives levels with a property no partition heuristic can claim: two hashes at the same level cannot depend on each other, because a dependency would raise the later one's depth. So the levels ARE the available parallelism. From the level sizes the report prints the ideal wall at 1/2/4/8/16/30/64 workers (the list-scheduling bound), the critical path, and the speedup ceiling. It also counts the const-pool hazard: constants are interned across the whole program, so a contiguous partition has cross-block read edges into `Const` cells. Hoisting them is sound only because a `Const` reads nothing, which is now a test rather than an assumption. Test-only, no production path. Folded into `census_and_panel` behind `LFM_REACH_PROFILE`, off by default, so it profiles the same programs the chip panel already describes — every wrap, every interior node, the slices, the parent and the root — with no new fixture plumbing and nothing a timed arm pays. `LFM_RPX_NS` supplies the box's permutation cost. Gates that fail without the code: removing the depth increment fails `the_profile_reports_a_known_chain_structure` (four independent chains of three must read as three levels of four) and `a_single_chain_has_no_parallelism_to_find` (its counter-case). The bound counts permutation steps only and charges nothing for memory traffic, record appends or scheduling. It is a floor on a parallel executor's hash phase and a ceiling on the speedup, and a measured arm still has to earn it.
`trace_identity_tests` pins the row walk: a chip's trace is a pure function of the records, so which walk fills it may not change one cell. The stage before it has no such gate — the records themselves are produced by a single serial `for` over the program, and nothing says what a different evaluation order owes the first one. A level-scheduled executor is about to need exactly that. This is the comparator, the case list and the vacuity guards, with both arms still calling the serial `execute`. It passes by construction today and that is the point: everything a schedule change has to land against is cheaper to get right before there is a second schedule than after, and a gate written beside the change it is meant to catch tends to be shaped by it. What is compared is everything an `LfmExecution` carries: every address through `WriteOnceMemory::get`, unwritten included — the occupancy bit is now the only thing separating "never written" from "written zero", so an address that lost its bit would read back as a legal zero and only this catches it — the const counter, all ten record vectors element for element, and `public_words`. Elements go through their derived `Debug`, which prints a felt's RAW `u64` rather than its canonical residue, so the assertion is bit equality rather than congruence: two executions of one instruction stream do the same arithmetic in the same order and owe each other the representation, not just the value. It also transcribes no record type's fields, so a row that grows a column is compared on it the day it grows one. Two guards decide whether a green run means anything. The first is the coverage list the sibling file already carries, ported: a chip with no records is compared vacuously. The second is new and is the one that matters here — a schedule can only be wrong where there is a choice to get wrong, so the cases must supply a DAG with width and depth to get wrong. They supply 15 and 14, measured by the reach profile rather than assumed, against floors of 8. That number is also a finding, and it constrains the schedule: a parallel executor wants a cut-off below which a level runs serially rather than paying a fork/join for one permutation, and any cut-off at or above 15 would send every level of every case here down the serial path. The candidate arm has to be reached with that cut-off lowered, or this file gates nothing. `Case` and `cases()` become `pub(super)` so the two gates run over one case list. A second copy would drift, and the failure mode is a case that quietly stops covering a chip on one side only.
The executor is one serial pass over the program, and ~83% of it is software RPX: 624k-691k of a wrap's 5.3-5.7M instructions are `Instr::Hash` and each is one full permutation. The reach profile measured what could run at once and the answer was not a guess: grouped by the longest chain of DEPENDENT hashes ending at each instruction, a wrap has 2,237 levels, 459 of them 512-17,091 wide holding 98.7% of the permutations, and two hashes at one level cannot depend on each other because a dependency would raise the later one's depth. So the levels ARE the parallelism, exactly, with no partition heuristic and no soundness argument to make. This runs them. The protocol is the part worth reading. A level's hashes are computed but not applied: the workers take `&WriteOnceMemory` and hand back rows, and the calling thread publishes every output cell and every record slot before the next level starts. Three things fall out that would otherwise have had to be prevented. No data race is expressible, because no `&mut` to the memory exists while a level runs and the borrow checker rejects a worker that tried to write. A wrong schedule is a deterministic error rather than a race: a hash launched before its input is applied reads an unwritten cell and gets `ReadBeforeWrite`, the same address on every run. And `DoubleWrite` and the occupancy bitset are untouched, because every write still goes through the one `write` on one thread. That last point is also why there are no atomics here: making `written` an `AtomicU64` would put a read-modify-write on all ~6-9M of a wrap's writes, on the serial path too, to protect a word this design never shares. There is no `unsafe`. Level order is not program order, so the records cannot be appended as the walk goes or the trace fill would be handed ten permuted vectors. Every arm writes the slot the schedule assigned instead. That would have made the old length-equals-census assertion vacuous, since the vectors are sized up front, so the check moved to where it is now stronger: the schedule counts the rows it hands out per chip and compares those to the emitted column-group counts, which says the same thing, earlier, and about the schedule rather than the vector. Narrow levels stay on the calling thread. 1,767 of a wrap's 2,237 levels are at most 16 wide and hold 1.1% of the hashes; serially those cost ~17 ms, on rayon ~4 ms plus 1,767 fork/joins, so the two are within ~10 ms of each other on a ~450 ms budget and the serial branch wins on the tie-breaker that matters -- it removes 79% of this executor's interactions with a pool that up to four sibling proofs are sharing. The cut-off is a parameter rather than a constant because it decides whether a test can see the parallel path at all: the laptop cases are 15 wide at their widest, so the production 16 would send every level of every one of them down the serial branch and the gate would go quiet. `execute` keeps its signature and reads `LFM_EXEC_PARALLEL` for the default; `execute_scheduled` takes the schedule explicitly, the way `build_traces_walked` takes a `Walk`, because the environment read is cached in a `OnceLock` and a test that flipped it would gate whichever arm ran first. The serial loop stays in the file as the reference, and both schedules share one transcription of every instruction arm and of the hash semantics. The depth pass keeps one `u32` per address rather than the profile's writer index plus per-instruction depth -- the same answer in half the memory, and an unwritten read then falls out correctly instead of needing a sentinel. It uses new non-allocating `Instr::reads_into`/`writes_into`; a `Vec` per instruction is 5.3-7.4M allocations per proof, and the existing `reads`/`writes` become thin wrappers so there is still one transcription of the operand conventions. Gated by `exec_identity_tests`, which now compares two real schedules, and by its mutation: merging adjacent depth levels must fail, at one address, every run. It does, and the address is one a hash writes -- the merge is offset so it pairs hash depths rather than collapsing the constants, which would fail for a reason that says nothing about hash ordering.
…fill
Two gaps in the level schedule, both found by a test rather than by reading.
`executor_rejects_addresses_outside_the_program` failed. An address past
`num_addrs` is legal to EMIT — the executor is what rejects it, a read as
`ReadBeforeWrite` and a write as `Internal("address out of range")`, and that
test pins both directions. The depth pass indexed its per-address array
directly, so it panicked on such a program before the executor ever saw it,
turning a rejectable program into a crash. It now uses `get`/`get_mut`: an
out-of-range read contributes depth 0 and an out-of-range write records
nothing, which leaves the rejection exactly where it already was.
The other gap is a number nobody could have attributed. The level walk writes
record slots, so its vectors are filled with blanks up front — one extra pass
of stores over a few hundred MiB that the serial walk never makes — and that
pass sat outside all four phase timers. It would have shown up only as the gap
between `execute` and the sum of the phases, which is the shape of a cost that
gets blamed on whichever phase is nearest. It has its own field now, and the
split line prints the sum beside the parts so the two can be checked by eye
against `LFM PROVE`'s `execute`.
Two things the first box arm asked for, and the first one is smaller than its number looks. `setup` read 0.25-0.44 s per node against a predicted 0.02-0.06, which invites the reading that a third of a second is sitting there to be removed. It is not. The serial arm's setup is 0.10 s and that is the write-once memory alone, about 314 MB, so a first-touch pass runs at ~3.1 GB/s here; the parallel arm's extra 0.15-0.34 s is 0.5-1.1 GB of records. At 4 KiB a page that is ~250k minor faults, around 0.24 s of the total, and the serial walk faults those same pages too -- just inside its own loop, where no timer names them. What was genuinely extra was one redundant pass of stores: the records were pre-filled with blanks so the walk could assign into a live element. Subtracting the arms gives the same answer as the fault model, 0.09-0.17 s, from different inputs. So the records are no longer pre-filled. Both walks now allocate the same way, the level walk writes each row once into spare capacity, and `commit_slots` publishes the lengths at a single call site after the last instruction. The `unsafe` is two `set_len`s reached only on the success path, and what makes the uninitialised state unreachable rather than unlikely is that a `?` on the way out drops zero-length vectors: a half-written buffer is freed without a slot ever being read, and there is no value for a caller to inspect. Three existing things establish that every slot was written -- the schedule's per-chip row count is asserted against the census before anything runs, every instruction is scheduled exactly once, and the identity gate reads every element of every record vector -- and a new test pins the failed-walk half directly. The second is an instrument rather than a change. The hash phase read 0.36-0.67 s where the profile's ideal at 30 workers is 0.09, and a wall cannot separate "the box is busy" from "the schedule is wrong" although those want opposite fixes. The coalesced levels run the same permutation on the calling thread with no pool in the path, so timing them costs nothing that was not already being spent and gives a per-permutation figure for this box under this load. The ratio to the parallel phase is then the width the pool actually delivered, printed. Record bytes are printed beside it, computed from the census rather than guessed, and the row widths that multiplier rests on are pinned by a test.
…r-hold card trace Print-only, all three behind env knobs, no behaviour change and no byte moved. The pass-5 question is where the card is idle, and three windows could not be attributed at the tip: - `multi_prove` prints nothing about its own phases. `crypto/stark/src/ instruments.rs` already carries the breakdown and is compiled out unless `--features instruments` is named — the wrong shape for this question, because the number being attributed is the block record and the record is produced by a binary that does not enable the feature. `crypto/stark/src/prove_split.rs` is therefore always compiled and runtime-gated: `LFM_PROVE_SPLIT=1` prints one `PROVE SPLIT:` line per call, with the four phase walls separated from the per-table worker-second sums, and the host-only stretches (the main-root absorption, the OOD absorption) split out from the device phases they sit between. - the base prints `base: N epochs in Ts` for a three-stage pipeline — a single-threaded producer, two trace builders, one prover. `LAMBDA_VM_BASE_SPLIT=1` prints a line per stage per epoch, including `recv`, which is the prover thread (the only stage that reaches the card) sitting idle waiting for a builder. - the permit reports occupancy per level and nothing per hold. `LFM_CARD_TRACE=1` prints one line per acquisition with the phase name and the two wall-clock stamps that bracket it, so a 10 Hz `nvidia-smi` sample can be sliced into inside-the-hold and outside-the-hold. Every line carries unix-epoch stamps for that reason: the two logs being aligned are written by different processes, so a process-relative offset would need the reader to know a start it cannot see. Cost when the knobs are unset: one `OnceLock` load and a predictable branch per region, and no clock read. Every call site is at phase granularity. `prove_split`'s accumulators are process-global (the fused region's drivers are rayon workers, so a thread-local cannot see them), which is sound only while one prove runs at a time. That holds — the card permit spans `multi_prove`, and the base has a single prover thread — and rather than assume it the module counts concurrent proves and marks the line `OVERLAPPED` if two were ever seen.
…on the success path `multi_prove` has `?` early-returns, and `report` — which only runs when the prove succeeds — was the one place the in-flight count came back down. A failed prove would therefore leave it stuck at one, and every later line would be stamped `OVERLAPPED` by a prove that FAILED rather than by two that overlapped. A falsifier that fires on the wrong condition is worse than none, because it reads as evidence. `ProveMark` now decrements in `Drop`, which covers both exits.
Level 0, every interior level and every node are bracketed by a `HostSampler`. The base is followed by `mark()`, which is a LIVE figure and is labelled `L_bundle` for exactly that reason: it measures the RETAINED bundle, after the prove's transients are gone. So the base's PEAK has never been measured in this driver — and it is the missing term in the only arithmetic that can decide whether the base and level 0 are allowed to overlap: `base peak + K × (the in-phase wrap footprint, 5.18 GiB) ≤ the 52 GiB stop`. Without it the base-wrap pipelining lever cannot be sized, only guessed at. The line names its stage mode, because on a LOADED base the window brackets a deserialize rather than a prove and the peak then says nothing about proving.
…ng them The pass-5 read of `r4_grind` had to argue from scale — 8.5 ms per table against a ~105 ms host floor at BLAKE3's 100 ns and ~5,830 s at RPX's measured 5,561 ns — to conclude the device arm fired. That is a sound inference and it should not have been one: `gpu_lde::GPU_GRIND_CALLS` already counts exactly this (one per table whose round-4 nonce search ran on device AND passed the host validity check; a device miss falls back to the CPU search and is not counted) and was never printed anywhere. The line now carries `r4_grind Xs (n/airs on device)`. n = airs is the device arm firing on every table; anything less names how many fell back. `r4_grind`'s doc now also says, in the place someone will read it, that the field is a Σ over tables and carries the two host floors — because the band this lane pre-registered against it was written per call and could not be scored. ⛔ The delta helper is tested against the bug its own first draft had: a swap followed by a load of the same cell returns the value just stored, so the delta is identically zero and every line reads "0 on device" whatever the device did. A counter that always reads zero is indistinguishable from a device arm that never fires, so the test asserts the second call sees only its own share.
The pass-5 profile found 10.4 s at 3.8% GPU utilisation between the global L2G prove ending and the first wrap taking the card — the largest contiguous idle block in the run, 4.3% of the block, and nothing measured it. It could only be decomposed by subtracting assumed terms, which is the move this campaign keeps having to retract. Three stamps close it, all reusing `LFM_CARD_TRACE` rather than adding a knob, because it is the same job: hand an external sampler two wall-clock stamps to slice itself by. - the bundle cache write. ⛔ HARNESS-ONLY and inside the `base:` number: serialising and writing a 19-epoch bundle is multi-second disk work no production pipeline does, and until now it was indistinguishable from proving. - `EpochConstants::load` — the ELF parse and the DECODE commitment, hoisted once for the whole walk. Real work, on the critical path, card idle throughout. - each wrap's pre-device prologue (reconstruct + emit). Its DURATION already printed; its POSITION did not, so it could not be matched to a sampler window. Every wrap carries it, which shows the ramp's shape rather than only its first term. `device_permit::trace_enabled` becomes `pub` so one knob drives both.
…at every level boundary `VmRSS` cannot separate "the prover is holding this" from "the allocator has not returned it yet", and that ambiguity is the whole of the interior's rising-peak question. The per-level host peaks climb 43 → 45 → 47 GiB while the levels SHRINK 10 → 5 → 3 nodes and the node census FALLS (525.9M → 456.2M → 437.6M cells), and level 2's rounds 1 and 2 hold an IDENTICAL two live nodes while reading 2.45 GiB apart — which residency cannot do, but which `VmRSS` also cannot prove, because it sees one number. jemalloc sees both. `stats::allocated` is bytes the program asked for and has not freed; `stats::resident` is what the allocator holds in pages. `resident - allocated` IS the retention, directly — no purge arm, and no inference from the census as a proxy. A level whose retained figure grows while its allocated figure falls is the allocator, not the prover, and the line says so in one read. Printed at every level boundary, at level 0, and after the base — beside the RSS marks that are already there, so the two readings sit on the same line of the log and cannot be quoted independently. ⛔ `epoch::advance()` first, always: jemalloc's statistics are cached, and a read without it returns whatever the values were when the epoch last turned — a number that looks live, updates sometimes, and lags arbitrarily. `#[cfg(test)]`-only by construction: `tikv-jemalloc-ctl` is a dev-dependency and `lib.rs`'s `#[global_allocator]` installs jemalloc under the same cfg, so these numbers describe the allocator that is actually running.
…ne builds the release C5 proposes dropping a table's Round-1 LDE once its root is absorbed and rebuilding it inside the fused task, so the gate's budget is not spent on tables that are merely waiting. Its cost is one extra coset LDE per released table; its benefit is bounded by the 27.1 s of Round-1 card idle. The ratio decides it, and it is a measurement. ★★ The SCOPE is decided before any measurement, and it decides C5. The block runs 64 proves whose AIR counts sum to 1,109 tables, so the break-even is 24 ms per rebuild for an all-tables policy and 423 ms for the heaviest table only. A forward NTT over LFM_HASH's 2^20 x 329 at blowup 4 touches 1.38 G base elements, nowhere near 24 ms — so the all-tables policy is dead on arithmetic, before the probe runs. But one table is 83% of the Round-1 budget, so releasing that one is most of the admission win and a top-1 policy has 17x the budget. Anyone who builds C5 all-tables has built the dead version. `coset_lde_row_major_no_tree` is the operation a release would actually re-run: at the barrier the tree is already built and its root absorbed, so only the LDE comes back. ⛔ It synchronises, and that is the point — the launches are async and a caller timing them without the sync would clock a queue submission and report the rebuild as free. The probe walks a LADDER rather than three named tables, because C5's decision is per table and a curve outlives a census. `C5_PROBE_SHAPES` overrides it. ⛔ Two checks that make this a test rather than a smoke run: it asserts at least one shape was measured (without a card the loop prints nothing, returns, and reads as a clean pass — which is how a probe comes to be quoted as evidence that C5 is cheap), and the module is gated on cuda so a non-cuda build cannot silently compile a probe it can never run.
…aries
The boundary snapshots answered the floor question and cannot answer the spike
one: every level from 2 up peaks in its FIRST ROUND and drops 2.7-3.4 GiB for the
rest, and by the time a boundary snapshot runs the spike is over.
It is not residency — level 2's rounds 1 and 2 hold an IDENTICAL two live nodes
and read 2.45 GiB apart. Sampled per node instead, the three candidates separate
in one read:
allocated spikes ⇒ LIVE, the prover really holds it
only resident spikes ⇒ jemalloc dirty pages, and a decay knob fixes it
NEITHER, but RSS does ⇒ outside jemalloc — the pinned staging slabs, the
retained device pool, the driver
The third is not a guess: ✓ `Backend::pinned_staging` is per-rayon-worker and
"grows lazily to the largest LDE the worker has seen", never shrinking, and that
memory is `cuMemHostAlloc`'d — counted in RSS and invisible to jemalloc. A new,
larger proof shape grows a slab on first encounter and later rounds reuse it,
which is a first-round-only spike by construction.
⚠ Its signature is also the one thing arguing against it: that story predicts
spikes SHRINKING as shapes repeat, and the measured spikes GROW (2.15 → 2.67 →
3.40) while both the node count and the census FALL. So it cannot be the whole
story, and this line is what says which part it is.
…alsifier The interior's host floor rises 19.3 → 28.9 → 31.5 → 32.7 → 33.7 → 34.2 GiB of LIVE allocation across levels holding 19 → 10 → 5 → 3 → 2 → 1 children. Neither "all children freed" (which predicts a falling series) nor "none freed" (40.7 by level 5 against a measured 34.2) reproduces that shape. A monotone, insert-only, SHAPE-KEYED accumulator does — and two exist, both process-global with no eviction: `domain_twiddle_cache` and `precomputed_tree_cache`. Both are insert-only, so the entry count IS the cumulative miss count. Entries plateauing while `allocated` keeps rising REFUTES the hypothesis; entries and `allocated` rising together with both increments shrinking supports it. Either way the reading is a subtraction rather than an argument. ⛔ `crate::tests::domain_cache_stats` already counts hits and misses and cannot answer this: it is `#[cfg(test)]` on the `stark` crate, so it is compiled out whenever `stark` is a dependency — which is every LFM run. It has never observed one. These accessors are always compiled. Printed on the line that already carries allocated/resident, so the cache count and the live bytes it is meant to explain can never be quoted apart.
…entries Lane C's correction is the sharp one: the cache is keyed by the precomputed ROOT, and in recursion every level proves N DISTINCT programs (a child's label is a program constant), so the program-dependent tables would MISS on every proof forever — one insert per proof per table, never hitting, never evicted. Its own doc says it was built for the BASE's repeating DECODE/BITWISE/range trees, which are execution-independent; the recursion tree is not that workload. That is a claim about hit BEHAVIOUR, and an entry count only proxies it — two caches with identical entry counts can have opposite hit rates. Counting hits and misses tests it directly, and it is cheaper than the byte total lane C asked about, which is not reachable: `MerkleTree::nodes` is private and the cache is type-erased, so bytes need a downcast per entry per backend. ⛔ Counted on the DOWNCAST result, not on the map lookup: a key that is present but holds another backend's tree is a miss to the caller, and counting the lookup would report a hit the caller never got. Reading: near-zero hits across the tree levels ⇒ a proof-count-linear accumulator, and eviction at harvest is a lever that does not compete with L5. A high hit rate ⇒ it is not the accumulator and the interior's rising floor is something else.
Measured on the block tree: the cache reached 357 entries at ~99.7 MiB each — essentially ALL of the 34.2 GiB of live host allocation at the end of a block — and it is what made the interior's host peaks rise (43 → 47 → 49.5 GiB) while the levels SHRANK from 10 nodes to 3. The recursion inserts 7–9 program-dependent trees per proof whose roots never recur, because a child's label is a program constant and every node proves a distinct program. It still hits ~35% there, on the shared execution-independent tables, so the cache is neither dead weight nor saturating — it is a useful cache with an unbounded tail. `LFM_PRECOMPUTED_TREE_CACHE_CAP=<entries>` bounds it. UNSET = unbounded = the behaviour before this commit, so a control arm is the same binary with the knob absent. `0` reads as unset rather than as "cache nothing": a zero-size cache would miss on every lookup, which is a typo nobody means to make. ✓ Eviction is SEMANTICALLY FREE, and the cache's own doc is the argument: the lookup key IS the root a rebuild would be checked against, so a hit needs no re-verification and a miss is only a rebuild. Nothing a proof commits to can move. ★ LRU by recency of USE, not of insertion — hits refresh the tick. Evicting by insertion order would throw away exactly the shared tables that keep hitting and keep the program-dependent ones that never will, which is the opposite of the point. The eviction test is written against that bug specifically: it touches the oldest key before the overflowing insert, so insertion-order eviction fails it. ⛔ `precomputed_tree_insert_capped` takes the cap as an ARGUMENT rather than reading the knob, so the tests exercise a real cap. The live cap is a process-wide `OnceLock` from the environment; a test that could only reach it that way would exercise the UNBOUNDED path and pass whatever the eviction did. The line that already reports the cache now carries evictions beside hits and misses, because the falsifier for the whole lever is that MISSES RISE — a cap below the working set — and those are the two numbers that say so.
Pure extraction, no behaviour change: the 493-line stage that proves the root's
extra child moves out of the tree driver into `prove_global_child`. Nothing else
in this commit.
# Why a signature is the point
✓ VERIFIED the stage reads nothing any interior level produces: `real_global`
takes the base bundle and nothing else, and the region never mentions `children`,
`layouts` or `labels` outside a comment. That independence was always true and
always INVISIBLE — the code sat wedged between level 0 and level 1, where only
its POSITION said when it could run, and a reader had 493 lines to check before
believing it could run anywhere else.
Now everything it needs is in seven parameters, so "can this run beside level 0?"
is answered by reading the signature. That question is the next commit's; this one
only makes it answerable.
# Two boundary facts the cut exposed, both of which change the shape
1. ⛔ `stage_mode` is a CLOSURE in the caller, over `lo` and `cache_dir`, and the
region called `stage_mode(0)`. Passing the closure would drag the caller's
cache policy in; the region only ever wanted LEVEL 0's mode, so that is the
parameter — `level0_mode: CacheMode`.
2. ⛔ `LFM_TREE_SIZE_GLOBAL`'s arm ENDS THE RUN with a bare `return`. A function
that produces the root's child cannot return nothing and still be read as
having produced one, so the return type is `Option<(RealGlobal, RealChild)>`
and that named stop travels as `None`, re-raised by the caller as the same
`return`. `LFM_TREE_STOP_AFTER_GLOBAL` stays in the caller for the same reason
and was never inside the cut.
⚠ I set the cut boundary 29 lines too late on the first pass, which put the
STOP_AFTER_GLOBAL block — and its `t_all` / `ceiling` / `whole_run` captures —
inside the function. It was the block's TAIL that said so, not the compiler,
because the tail still parsed. The cut is now `real_global` through
`mark("AFTER the global child")` and nothing past it.
Card-free tests green (15), `make lint` and `make fmt` to follow on the branch tip.
…e after it Lane P5 priced the top stages at ~10 s of wall at 39.8% card utilisation, wedged between level 0 and level 1 at K=1 — a pool of 6.0 s. `prove_global_child` reads only the base bundle, so it can run beside any wrap; `LFM_TREE_TOP_OVERLAP=1` makes it task 0 of level 0's existing pool. ⛔ ONE MORE TASK, NOT ONE MORE WORKER, and that is the whole memory argument. A thread beside the level would put `l0_siblings + 1` host working sets on a 57.53 GiB box against a 52 GiB stop — a term not bounded by K. As an item in the SAME pool at most `l0_siblings` are ever live, and one of them is a slice INSTEAD of a wrap. The card is unaffected either way: the global task takes the same permit every wrap takes, so device concurrency is still K. ⛔ INDEX 0, so a free worker picks it up immediately. It is ~10 s against a wrap's ~14.6 worker-seconds; queued last it would BE the tail and the lever would pay for itself twice. PREDICTED, from the p5c1 host-peak lines rather than from the summary: the wrap stamps grow 27.255 → 34.553 GiB across the level, which fits ~0.487 GiB per RETAINED wrap. That pins the retained term; it does not pin the live one, and two defensible splits of the baseline give an overlap peak of 38.0 or 43.9 GiB. ⇒ The NUMBER is underdetermined and the DECISION is not: every reading is comfortably under the 52 GiB stop. Falsifier stays > 48 GiB. Wall: level 0 is 19 × 14.56 = 276.6 worker-seconds over K=4 = 69.2 s in a 76.9 s wall; +10 s of task = 71.6 s, so level 0 grows 2.0-3.5 s and the 10 s stage goes. Band −5 to −8 s. ⚠ The top edge is bounded by 10 − 10/K = 7.5 s, because the stage's host half does not vanish — it becomes worker time inside the level. The drain is `split_pool_out`, named and tested rather than inline, because the order is the point: `children`, `layouts` and `labels` are three parallel vectors the interior indexes by POSITION, so a wrap at the wrong index is a node built over the wrong subtree — and the IDENTITY lines would still print, about a different tree. Tests, all card-free and all forcing what they check: - `split_pool_out_keeps_index_order_when_completion_is_reversed` — 9 tasks with completion forced to reverse index order and the odd task in the MIDDLE, where an off-by-one in the index shift still looks right at an end. - `the_overlap_does_not_move_a_single_wrap` — a pool of 9 against a pool of 10 whose task 0 is the global, asserting the wrap sequence is identical. That is the IDENTITY gate's precondition, at unit scale. - `a_panicking_global_task_re_raises_with_its_message` — the global used to abort a K=1 stage with its own message and must not become "a scoped thread panicked" by moving. - `a_missing_global_task_is_caught_at_the_drain` — the OFF arm's assert, so a knob that quietly stopped scheduling the task fails at the drain instead of at the root with no child to give it. Unset is today's shape, so the control and candidate arms are one binary.
clippy::needless_option_as_deref, caught by `make lint` and not by `cargo check`: the extraction made `cache_dir` a parameter of type `Option<&str>`, so the `as_deref()` the inline stage needed is now a no-op on its own type.
…level Pure extraction, no behaviour change, and the same move that made L3 safe: `prove_one` sliced `&children[g]`, `&layouts[g]` and `&labels[g]` out of the level loop, and those three captures are exactly what tied a node to the LEVEL being the unit of scheduling. They are parameters now. ⇒ A caller holding ONE node's children — rather than a whole level's — can prove it. That is all `LFM_TREE_LEVEL_POOL` needs from the driver, and this commit is only the naming so the scheduler that follows can be read against a body that did not move with it. `siblings` rides along as a parameter because it decides one PRINT: whether the node's host-peak line says "process-wide, N proofs in flight". A wrong number there is a reader believing a concurrent reading is a solitary one, which is the error the line was added to prevent. `NodeSlot` is hoisted out of the loop with it, for the same reason.
…ls-in-flight cap `prove_in_dependency_order` replaces the interior's per-level barrier with a pool over the whole tree: a node runs when its own two children are done, not when its whole level is. Lane P5 measured the barrier's cost at 6.1 s of between-hold idle over levels 2-5, where 5, 3, 2 and 1 nodes have to fill two workers. ⛔ AND THE BARRIER IS ALSO A RETENTION POLICY, which is the larger half. Today a level holds ALL of its children until it ends — `children` is a Vec alive across the level and every node borrows a subslice. In a TREE each child has exactly ONE parent, so here a node TAKES its children and drops them when it returns: 19 wraps released pairwise as level 1 proceeds instead of all at once at its end. That is the `floor` term the profile says no purge setting touches, and removing it is a prediction this lever can be falsified on. ⛔ A NODE RETURNS TWO THINGS, and the take is what forces it. Taking a child means it is GONE once its parent has run, so a scheduler that frees children cannot also hand every level's values back — they are the same bytes. Each node returns `(value, summary)`: the value is what its parent eats, the summary is what the log needs and is kept for every level. Only the TOP level's values survive, because only they have no parent. ⓘ I had it returning every level's values first, and the tests said so: the drain asked level 1 for its values and level 2 had already eaten them. The failure was the design telling me what it costs. THE CAP. A node at level L waits until every level at or below `L - M` is COMPLETE. At M=1 that is "level L-1 complete before any node of L starts" — the barrier exactly — so M=1 runs this scheduler on the OLD schedule and isolates the scheduler's own cost from the overlap's benefit. It cannot deadlock: a node at the lowest incomplete level is never blocked, since every level below it is complete by definition, so the cap always admits some work. Four gates, each forcing what it checks rather than hoping for it: - `a_node_never_starts_before_both_its_children_are_done` records every start against its children's finishes, with UNEQUAL child sleeps so one leg of every pair is genuinely late. Without the forcing it would pass on a scheduler that happens to finish pairs together. - `one_level_in_flight_reproduces_the_barrier` asserts no node of L starts before every node of L-1 ended — the property that makes M=1 a usable control. - `two_levels_in_flight_actually_overlap` asserts the opposite at M=2, because a cap that silently blocked everything would look exactly like a correct barrier and the test above would still pass. - `a_panicking_node_re_raises_and_does_not_hang` — the message survives, and the other workers do not sit on an empty queue. Not wired to the driver yet; that is the next commit, behind `LFM_TREE_LEVEL_POOL`. Three re-runs at `--test-threads=8`: green.
…_LEVEL_POOL Wires the dependency scheduler into the driver. `LFM_TREE_LEVEL_POOL=1` hands levels `LFM_TREE_LEVEL_POOL_FROM..=hi` to the pool; the barrier loop keeps the levels below it, so the insurance row (FROM=2) is the same code with a different boundary rather than a second implementation. Unset, `barrier_levels == hi` and the loop is the whole interior byte for byte as it shipped. ⚠ WHAT THE POOLED SPAN CANNOT PRINT, and it is a real loss rather than an oversight: a PER-LEVEL host peak. Two levels running at once share one process, so "level 3's peak" stops being a quantity. The span reports ONE window, labelled as one, plus the per-NODE peaks the nodes already print. ⇒ The stop condition has to read the node lines and the span line; a per-level maximum to compare against the control's no longer exists, which is worth knowing BEFORE the arm rather than when someone greps for a line that is not there. ⛔ AND THE IDENTITY LINES ARE FORMATTED ON THE WORKER, PRINTED AT THE JOIN. The child is about to be eaten by its parent, so the line must be taken while it exists — but printing it there would put it in COMPLETION order, which is exactly what the gate may not depend on. Formatted early, buffered, printed in level and index order after the span. The ordered diff against a barrier run is therefore empty, not merely sortable. ⛔ REFUSED WITH `LFM_TREE_SIZE_ROOT`, not silently disabled. The sizing arm holds two levels' outputs at the top and picks them BY LEVEL INDEX; a pool that frees a level into its parent has no such index to hand out, and the failure mode is a root built over the wrong children — which `emit_l2g_compare`'s count guard catches only when the shapes happen to differ. The assert names both knobs. Card-free gates: 23 pass, including the scheduler's four and the level-0 pool's four. `make lint` + `make fmt` to follow before I name this a ready sha.
…'s completion Lane P5's boundary snapshots (0e523b7) settled what the interior's rising floor IS: allocated climbs 19.35 → 28.92 → 31.50 → 32.71 → 33.65 → 34.24 GiB across the levels while jemalloc's own retention (resident − allocated) stays at 0.37-0.79 GiB throughout. So it is LIVE bytes, not allocator retention — the 19 wraps are still allocated after level 1 ends, because the barrier driver holds every level's children to the end. ⇒ That is the retention policy take-on-consume replaces, and `allocated` is the instrument that tests it directly. The whole-run peak cannot: ~12 GiB of the 47 GiB process peak sits OUTSIDE jemalloc (pinned host pool, mmaps), so the peak will not fall by the allocated delta even when the mechanism works perfectly. ⛔ The barrier loop already prints this per level; the pooled span did not, and that is exactly where the falsifier lives. A level's completion inside the pool is a MOMENT in the middle of the span, not the end of a loop body, so the scheduler gained an `on_level_done` hook and the driver prints the line from it. ⛔ The hook is called UNDER THE SCHEDULER LOCK, deliberately. The number's whole meaning is "at the instant this level finished"; letting a worker start the next node first would price a different moment. It is one mallctl read and one print. PRE-REGISTERED, from lane P5's lines: after level 1 completes in a pooled run the 19 wraps should be GONE — allocated ≈ 12 GiB against the barrier's 28.92 at that boundary, a −16.9 GiB delta — and every later boundary should read one level's live children plus the bundle rather than the cumulative sum. ⛔ FALSIFIER unchanged and now sharp: if allocated at that boundary is still ~29, retained children are not a floor term and the model behind the whole interior memory story is wrong. Rebased onto 0e523b7 so the lines exist on this arm at all; all six commits re-signed.
… shown the take
Two defects the arm found, one in the lever and one in the instrument I built for
it. The second is the more useful.
1. ⛔ THE POOL READ ITS WORKER COUNT AFTER THE INTERIOR WAS DISARMED. The driver
arms the permit at `siblings_wanted` before the level loop and re-arms it to 1
immediately after ("the interior is done; level 0 and everything after it run
serial"). The pooled span was inserted BELOW that line, so
`device_permit::workers()` returned 1 and the arm ran the whole interior
serially: 21 nodes in 103.0 s against the barrier's ~79 s, +20 s on the block.
⇒ The span moves ABOVE the disarm. That is also the only correct place for it on
the card's terms: the permit has to be armed at the interior's count while the
pool runs, or every node serialises on the card whatever the worker count says.
ⓘ Every other number from that arm is a K=1 number and none of it is bookable —
including the 43.9 GiB peak, which is the one-worker live set.
2. ⛔⛔ AND THE BOUNDARY INSTRUMENT COULD NOT HAVE SHOWN TAKE-ON-CONSUME AT ALL,
whatever the worker count. The barrier loop does `children = next` at :5959 and
prints its jemalloc line at :6001 — it frees the previous level's children BEFORE
it measures. So both schedulers are structurally forced to agree at a boundary:
the barrier frees them all at once just before the reading, the pool frees them
progressively, and the reading is taken after both are done. The pooled series
matching the barrier's to 1 MiB is that agreement, not a failed take.
⇒ A check that cannot fail, built by me, to test my own prediction. The two arms
could not have differed there.
★ THE SIGNAL IS INSIDE THE LEVEL, NOT AT ITS EDGE. Both paths now print
`L{n}N{j} after-release` per node, at the same logical point — one node finished:
· in the POOL, after an explicit `drop` of that node's children, so the line
falls as level 1 proceeds;
· in the BARRIER, where the level still borrows every child and the line is FLAT
by construction.
The CONTRAST between the two per-node series is the measurement. That is what the
falsifier should have been aimed at from the start, and the boundary number —
mine and the revised one — was aimed one step too late.
Card-free gates 23/23; `make lint` to follow before this is a ready sha.
…they answered
Lane P5 withdrew the children column and the coordinator withdrew the 18-19 GiB
floor falsifier with it. A `RealChild` is proof-scale — roots, log heights, chunk
counts, hasher, chip set, options, public words, per-table openings, legs, and no
LDE, no trace, no tree — and the "1.018 GiB per wrap" that made it look otherwise
came of dividing level 0's total by nineteen without subtracting the 6.5 GiB
bundle that was live at the same moment. The floor under both schedulers is the
precomputed-tree cache (26 entries after the base, 201 after level 0, 357 at the
end, never evicted, ~101 MiB a tree) plus live proving state, which is a
stark-side lever and not this driver's.
So the per-node `L{n}N{j} after-release` line prices a difference that was never
going to be at GiB scale, in both paths, at twenty-one lines of output an arm. It
goes. An instrument outlives its question only while someone is still asking it,
and nobody is.
★ WHAT STAYS IS THE RELEASE ITSELF, with a comment that now claims only the
mechanism: these children were TAKEN out of the level below's slots, so the node
owns them alone and they go the moment it is proved, rather than at the end of a
level that borrows every child. That is the property which lets two levels be in
flight without two levels of children being live, and it belongs where it
happens.
With both knobs unset the file prints exactly what `0e523b78` prints — every line
this branch adds sits inside `if pool_on` or `if top_overlap` — so the control arm
is unchanged and the byte gate reads the same forty IDENTITY lines.
`make lint` 0, `make fmt` 0, and 16 of 16 card-free gates in the module pass,
including all nine written for L3 and L5. The module's two other tests fail here
for a missing `continuation-fixture.elf`, which is untracked and absent in every
worktree on this machine; they are environmental and predate this branch.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Draft: the per-table GPU recursion, end to end — block 25368371 compressed into one root proof, and five optimization passes.
What this is
The full per-table pipeline on the GPU: the epoch base proofs, the epoch wraps, the interior aggregation tree, the block-wide memory argument (as slices and a parent), and the block-artifact root. Every stage is proved on the card; the root is proved and verified. This branch is for sharing the work — not for merging yet.
Block 25368371, 19 epochs at 2^21 rows, fan-in 2 → 19 wraps, 21 interior nodes in 5 levels, 2 global slices, their parent, one root.
Times
Ryzen 9 9950X + RTX 5090,
TABLE_PARALLELISM=4, one arm per process, nodes within a level proved serially. "Before" is the first end-to-end of the pipeline; "pass 1" (8a59fa1d) and "pass 2" (4fcb3341) are the tips of the first two optimization passes; "pass 3" (7a4ec7e7) the third; "pass 4" (3a1ae471) the fourth; "pass 5" is this branch's tip (ca4790c2) — each measured end to end on the same box from a fresh cache, every stage proved.Pass 3's record was reproduced within 0.1% on a second fresh-cache run (252.5 s). Pass 4 is a paired measurement on one binary: at
9b74c9ee(the lever without its slot-fill follow-up) the executor knob set to the serial path (LFM_EXEC_PARALLEL=0) runs the block in 251.7 s and the level schedule in 234.7 s; the tip3a1ae471reads 231.1 s on the same knobs. All 40 identity lines are byte-identical across the control, both candidates and pass 3's serial record; the whole run's host peak is 47.0 GiB.Pass 5 is scored on the run window, not on the stage sum: the lever that folds the global slices into the wrap pool removes inter-stage gaps that the printed stage walls never counted, so a stage-sum ladder would report it as −2 s where the measured wall fell −32 s. The closing measurement is a paired A B B A on one binary (
ca4790c2), the pass-4 configuration (four wrap siblings, two interior siblings, the slices as a separate stage, VRAM budget 16000, the per-level barrier, the unbounded precomputed-tree cache) as the control: 243.2 / 244.1 s against 211.0 / 211.6 s for the pass-5 configuration (six wrap siblings, three interior siblings, the slices inside the wrap pool, budget 24000, the interior dependency pool, the cache capped at 64 entries) — 243.7 → 211.3 s, −32.4 s, −13.3%, both candidates at least 31.6 s below both controls; the host peak 47.0 → 33.9 GiB; the device peak 24.8 → 26.7 GiB of 32.6; all 40 identity lines byte-identical, in content and in order, on all four arms. The pass-4 configuration's window on this binary (243.7 s) is 12.5 s above its 231.1 s stage sum; that offset is not a constant (6.4 s on another arm the same day), so the two metrics are never differenced against each other.On a Ryzen 7950X + RTX 5090 (16 cores, 120 GiB host) pass 3's commit runs in 9.3 min serial, 6.3 min at two wrap and two interior siblings, and 5.4 min at four wrap and three interior siblings — the third interior sibling peaks at 54.4 GiB of host memory, above the 9950X box's 52 GiB stop, so it is a 120 GiB configuration. Pass 4 on that box, same knobs, paired on one binary: 323.2 s with the serial executor, 295.1 s (4.9 min, −8.7%) with the level schedule; the wraps fall 10.6% there because sixteen slower cores are host-bound at four live wraps where the 9950X is not; 40 identity lines byte-identical; whole-run host peak 51.7 → 49.2 GiB. Device peaks and host peaks are the same on both hosts to within 1%, wall times are not — memory bands transfer across hosts, time bands never do. Recursion overhead — everything after the base proofs — is now ≈ 2.7× the base time (was 11× after pass 1, 5.2× after pass 2). The harness re-verifies every child and every proof it makes as a test precondition; measured in the serial run that is ≈ 66 s of host work (2.6 s per wrap, 0.7 s per node), and under concurrency it overlaps other work, so no production-equivalent subtraction is made for pass 3.
Where the time went, measured phase by phase before anything was changed (the profile is in the campaign's state file): the recursion was host-CPU-bound — the GPU read 0% in 91% of samples through the wraps — and the largest single phase was the preprocessed-column commit (
build_artifacts, an LDE + Merkle pass on the host, 43% of the block), followed by LFM program execution + trace fill (15%), the per-epoch reconstruction in the harvest (9%), and the STARK prover itself at 13% running at a healthy 57% device utilization.What changed in pass 1
prover/src/lfm/trace.rs): the per-chip row loop walkspar_chunks_muton rayon's global pool; every fill closure was read and is row-local; a cell-for-cell identity test against the serial reference covers all chips under RPX and BLAKE3 dispatch. 6.5× on the hash chip on an 11-thread laptop; on the box the per-node prove component fell 13.6 → 9.7 s with the artifact phase unchanged.prover/src/lfm/commit.rs):lde_columnsruns an explicitpar_iterover columns with interpolate→expand fused (one fewer copy of each group's coefficients); the group loop is windowed (LFM_ARTIFACT_GROUPS_IN_FLIGHT, default 4) with the memory reasoning kept. Roots are pinned byte-identical to the serial build by theregistry_drift_*tests. Per node:build_artifacts21.9 → 15.2 s.603c1e15) made byte-hash counts structurally zero; the register-derivation instrument now follows the block pin in all three places; the FRI-leg byteswap counts carry a hash width.crypto/math-cuda/kernels/rpx.cu,crypto/stark/src/grinding.rs): the 2^20-trial search ran on the host per table because the device arm accepted only Keccak — about two-thirds of each base epoch's CPU time (RPX costs 2,368 ns per permutation on the host) and ~1.4 s of every recursion proof. An RPX kernel loops the existing device permutation over a nonce range and returns the smallest valid nonce (atomicMin, deterministic), dispatched by the configuration's commitment hash; pinned by a no-GPU known-answer layer replaying the kernel againststark::grinding::is_valid_nonce(four kernel mutations each red) and three device gates, one of which asserts the dispatch actually reached the device. Same factor, same predicate — no security change. Base 156 → 68 s. This cost is specific to the RPX pin;maingrinds a Keccak-class digest and is unaffected.What changed in pass 2
prover/src/lfm/commit.rs,crypto/stark): the per-proof artifact build — coset LDE, leaf hashing and Merkle tree for every preprocessed column group of an LFM program — ran on the host, and after the RPX pin its Merkle half was RPX permutations on ~26 cores (56% of the phase). A named public entry point instark(try_commit_row_major) exposes the device's fused LDE + leaf-hash + Merkle for one row-major group, which is the layoutColumnGroupalready holds, so the host's strided transpose is skipped too; the host pass remains the fallback below the device floor (padded_rows × blowup ≥ 2^14, a row count) and underLFM_DEVICE_ARTIFACTS=0. Per proof the phase went 14.4 → 0.4 s on interior nodes and 9.8 → 0.3 s on wraps, withproveandharvestunchanged (5.9 s and 0.7 s per node before and after). Device peaks did not move: the artifact commit runs while the card is otherwise empty, and the device tree is freed beforemulti_provebuilds its own.registry_drift_*root pins (which reach the device exactly once per fixture, on the one program-independent group above the floor — evidence, not coverage), adevice_paritytest that commits a group above the floor both ways and compares roots at the production width extremes (1, 20 and 134 columns) after asserting its own premise, and the fixture-scale root test, which undercudanow refuses to pass if every group fell back to the host. The census line reports how many groups took the device path per level (groups D/T on device; a production wrap prints 8 of 12, a level-1 node 8 of 12) and the device set the build asked the card for. On every production proofmulti_proverebuilds the precomputed tree on the device and refuses on a root mismatch — the strongest witness, and it stayed silent on all 44 proofs of the record run.LFM_DEVICE_ARTIFACTS=0as the control): wraps 388.9 s host vs 206.2 s device; level 1 215.7 s host vs 75.5 s device.prover/src/lfm/proof_fixture.rs,bench_vs/lambda/continuation-fixture): the closure test's fixture guest committed at the very end of its run, so the "output half" of the check had no subject — a sibling fixture guest commits in an intermediate epoch and then does bounded work, and the fixture asserts its commit-to-boundary, boundary-to-halt and halt-to-end margins in the guest's own step currency (the epoch count never moved when this broke, so the two-epoch canary never rang). The R1d transcript-replay instrument is a byte sponge that names its hash directly, per the hash-pin carve-out; its count now reads the same named constant as its builder.What changed in pass 3
prover/src/lfm/per_table_aggregator_tests.rsdriver,prover/src/lfm/commit.rs,prover/src/lfm/proof.rs): after pass 2 the top of the block was four sequential host walks per proof (LFM program execution, epoch reconstruction, program emission, harvest — none of them parallel) with the device prover in between; the driver proved siblings one at a time. It now proves K siblings of a level at once, with a single mutual-exclusion permit taken around each proof's two device phases (the artifact commit andmulti_prove) and released between them, so one proof's host walks overlap the other's card time while the card never holds two proofs (the two-VramGates trap, closed at the callers by Fix A, is not reopened one level up: neither admission path keeps a cross-proof total, so the permit is exclusion, not a byte budget). K is a per-level knob (LFM_TREE_SIBLINGSfor the interior,LFM_TREE_SIBLINGS_L0for the wraps, both default 1 = the serial control); the census window enrols workers explicitly so a stray builder cannot inflate a level; the level line reports acquisitions, max holders, and the card's held share; each node prints its program identity (the digest a parent absorbs), heights and published words on one line, so byte identity between schedules is adiff.K_min = ceil(1 + host/device)— and it reproduces the measured card share at both interior levels (75% and 68% at K=2); a wrap wants four workers on time grounds and the host peak decides how many it gets.prover/src/lfm/executor.rs,proof.rs): the executor's record vectors are sized from the census the compiler already holds (one record per instruction per chip, exact), the write-once memory cell drops from 40 to 32 bytes with a bit-per-address written map (a read-before-write test now exists on the executor, not only the validator), and the executor's memory and records are freed before the card phase. Byte-identical (the identity lines diff clean); the executor is 3% faster per wrap and the level-1 host peak, the number that bounds a third interior sibling, falls from 48.2 to 46.6 GiB. The executor itself is 83% software RPX permutations (one full permutation per hash instruction, 644,250 per wrap at 2,356 ns each on the 9950X), so it is not a lever for layout work; the levers left were running those permutations on the parallel side or making one permutation faster — both priced before any code was written, and pass 4 is the first.execute · fill · multi_prove(recorded in a per-thread cell, printed by the driver), every wrap prints its own TIMING line and census (level 0 printed one number for nineteen wraps), the harness-only verification is timed rather than banded, and the permit wait is its own field. On an arity-2 level-1 node: executor 2.25 s, fill 0.27 s, device prover 3.4 s.What changed in pass 4
prover/src/lfm/exec_schedule.rs,prover/src/lfm/executor.rs,prover/src/lfm/instr.rs): after pass 3 the executor was the largest host phase left — one full software RPX permutation per hash instruction, 624–691 thousand per wrap, 83% of a 1.8–2.2 s single-threaded walk — and it ran while the card waited. An LFM program is a write-once, topologically ordered straight line, so one forward pass gives every instruction its depth in the chain of dependent hashes, and two hashes at the same depth cannot depend on each other. The executor now walks those levels: a level's hashes run on rayon's global pool holding only a shared borrow of the memory and hand back their rows; the calling thread then publishes every output cell and record slot before the next level starts, and the non-hash instructions of the level run serially in program order. Nounsafe, no atomics, no change to the write-once memory or its double-write check; a hash launched before its input would read an unwritten cell and fail deterministically at the same address every run, which is what the mutation test asserts. Record vectors are pre-sized from the census the compiler already holds and written by slot, so the records come out in program order whatever the schedule, and the trace fill sees the same bytes.reach_profile.rs, test-only) reads a program's hash DAG. A wrap's is 2,237–2,400 levels deep and bimodal — about 1,770 levels of width ≤ 16 hold 1.1% of the hashes (the Fiat–Shamir transcript, a strict chain), 459 levels 512–17,091 wide hold 98.7% (the query paths) — so the list-scheduling wall at 30 workers is 0.05 s against 1.5 s serial and the transcript chain binds nothing below ~260 threads. The other candidate lever, a vectorised Goldilocks multiply for a faster single permutation, was measured with a hand-written AVX-512 kernel (test-only, on its own branch): 1.7–2.0× the best scalar arm at the throughput shape a permutation has, but an 8-way permutation needs the same depth levels this pass builds and, after it, would reach under 0.5% of the block — closed as a lever, recorded as a number.LFM_EXEC_PARALLEL=0as the control, pass-3 knobs, fresh caches): the executor per wrap 2.10 → 0.92 s median under four live wraps (0.47 s at best), per level-1 node 2.25 → 0.63 s, per global slice 1.95 → 0.44 s. The block 251.7 → 234.7 s. The gain lands where sibling concurrency cannot reach: the single-proof stages at the top of the tree (slices, parent, root) −30%, levels 2–4 −15%, level 1 −7%, the wraps −3.5% — at every level with siblings the card is the wall, and the permit's held share rose (level 1: 75% → 80%). The executor's own split is printed per proof (LFM EXEC:— levels, how many ran in parallel and how many hashes they held, then depth pass · setup · hash phase · apply · residue); under four live wraps a wrap readsdepth 0.07 · setup 0.10 · hash 0.18 · apply 0.03 · residue 0.14. The tip writes the record slots without the zero-fill (spare_capacity_mutand oneset_lenper vector after the last instruction, under the invariant that any early return drops zero-length vectors, pinned by a test) and prints a third line — records MiB, the permutation's cost on the calling thread, and the effective width the pool gave the level phase. Read against its own pre-registered bands: setup fell 0.14 → 0.05 s per node, butexecutestayed 0.62 → 0.61 s — the record first-touch moved into the residue rather than vanished, which the bands said would be the honest outcome — and the effective width reads 9.4–9.8 of 30.7 threads on an uncontended node at two siblings, 4.4 while overlapping a sibling's fill, 4.6–11.5 per wrap at four. The executor stops being a lever here: the card's held share is 78–82% at every level with siblings and host time converts to wall at about a fifth, so the remaining executor terms are worth under half a percent of a level and are declined on the record, not deferred.What changed in pass 5
multi_prove(LFM_PROVE_SPLIT=1: the four phase walls and eleven per-table worker-second sums), one per base pipeline stage per epoch (LAMBDA_VM_BASE_SPLIT=1), one per card-permit hold (LFM_CARD_TRACE=1), and stamps on the three stretches between the base and the first wrap. All print-only, runtime-gated, always compiled, so the split is taken from the record binary rather than a feature build; every line carries unix-epoch stamps so the sampler's CSV slices directly. The card was busy 153 s of 241; of the 88 s idle, 27 s sat inside Round 1 ofmulti_prove(the main commit, where the VRAM gate admits only ~3 tables because one table is 83% of the budget), 17 s inside the fused rounds, 20.5 s in the K=1 stage between the wraps and level 1, 15 s in the base's own proves (the base pipeline is 98.3% packed — the prover thread waits on a trace builder for 1 s in 67), and the rest in ramps and tails. The base's card idle is inside its own proves, so a wrap's device phase cannot use it.prover/src/lfm/per_table_aggregator_tests.rsdriver,LFM_TREE_TOP_OVERLAP=1): the global child depends on the base bundle alone, and it ran as a K=1 stage after the wraps. Folded into level 0's existing pool with the worker count unchanged (one more task, not one more worker; the same card permit), the 20.5 s stage disappears and level 0 grows by the global's held card time, ≈ 6.6 s — the card is the wall at every level with siblings, so card time adds and only host time packs. Paired on one binary: −12.7 s.LFM_TREE_LEVEL_POOL=1,LFM_TREE_LEVELS_IN_FLIGHTdefault 2,LFM_TREE_LEVEL_POOL_FROMdefault 1): a node needs only its two children, so the per-level barrier's tails (a level of 10 nodes at three workers pays a whole round for one node) are overlapped with the next level's head; a node takes its children out of the level below's slots and releases them when it is proved. Identity lines are formatted on the worker and printed at the join in level and index order. Paired at the record configuration: −2.5 s on the run, −1.3 GiB on the host peak, ordering byte-identical.LAMBDA_VM_VRAM_BUDGET_MB16000 → 20000 → 24000 (−8.5 s then −2.8 s at a device peak of 26–28 GiB; the gate bounds construction, not residency, so a larger budget lets more Round-1 tables build at once while the resident set barely moves; the 29,000 MiB stop stayed silent on every arm). Each rung measured A B B A on one binary.crypto/stark/src/prover.rs,LFM_PRECOMPUTED_TREE_CACHE_CAP=<entries>, unset = the unbounded map): the interior's host floor rose from 19 to 34 GiB across the levels while the live child count fell, and the allocator held only 1–3% of it (jemalloc's live and resident bytes printed at every level boundary and per node; an eager-purge arm moved the peak −0.7 GiB at +1.8% wall). The cause is the prover's process-global cache of precomputed-column Merkle trees, keyed by root and never evicted: the recursion proves N distinct programs per level, so its program-dependent tables insert 7–9 trees of ~100 MiB per proof that never hit (357 entries, 316 hits / 472 misses by the end). An LRU cap of 64 keeps the shared tables that do hit (misses 472 → 474, 294 evictions) and is byte-free by construction — the lookup key is the root a rebuild is checked against, so a miss is only a rebuild. Paired on one binary: −0.5 s (noise), host peak 49.5 → 36.6 GiB.The root
LFM_HASHheightroot_schema_words(67, 40, AssertOnly)A is the default: 7% more root cells than B, but it retires the top node (one proof fewer, one level less latency). The option is an input (
LFM_TREE_ROOT_OPTION=A|B, refused when unset), not a ruling.Gates
At the arm's commit, in a box
--librun: 27 unit gates (the parent's 12 — z/α agreement, L2G-root agreement and republish, partials summing to zero, partition tiling, gap / overlap / stop-short, slice count both ways — and the root's 15, including the five pre-registered tamper arms), the honest control (two real slices and their parent, summed to zero), and the fixture-scale root proved over real children under both options. Mutation-tested: each tamper arm fires on exactly the check it names. The trace-fill identity test and the sixregistry_drift_*root pins gate pass 1's changes; pass 2 adds thedevice_paritygate and the fixture root test's device assertion (bothcuda-only, because without a card both sides are the host pass and the check could not fail).Caveats, by design
recursion::check_attestationbinds the proof to the block host-side, against an ELF the consumer trusts; the guest uses the supplied roots verbatim. "One proof for this block" terminates there.Running it
LFM_TREE_LEVELSproves or loads the interior levels; the global stage and the parent have their ownprove|loadmodes; Prove refuses to overwrite a cached entry. Knobs:LFM_EXEC_PARALLEL=0selects the serial executor (pass 4's control; unset or1is the level schedule);LFM_TREE_SIBLINGS=KandLFM_TREE_SIBLINGS_L0=Kprove K siblings at once in the interior / at level 0 (default 1, the serial control; the record runs 6 and 3);LFM_TREE_TOP_OVERLAP=1runs the global slices and parent inside the wrap pool,LFM_TREE_LEVEL_POOL=1runs the interior as one dependency pool (LFM_TREE_LEVELS_IN_FLIGHT, default 2, caps it;1reproduces the barrier through the pool),LFM_PRECOMPUTED_TREE_CACHE_CAP=64bounds the prover's precomputed-tree cache (unset = unbounded);LFM_PROVE_SPLIT=1,LAMBDA_VM_BASE_SPLIT=1andLFM_CARD_TRACE=1print the per-call, per-stage and per-hold splits with unix-epoch stamps;LFM_DEVICE_ARTIFACTS=0forces the host artifact build (pass 2's control);LFM_ARTIFACT_PARALLEL=0reproduces the pre-pass-1 host build exactly;LFM_ARTIFACT_GROUPS_IN_FLIGHT=Nbounds host residency.Not in this branch
The VRAM admission/scheduler decoupling and the barrier levers (
pt/barrier-levers) are separate; 2^22 needs the epoch wrap sliced the same way and is not attempted here. Also separate, built but not yet measured: the base's two device proves taking the card permit and an optional sink that streams each epoch proof as it completes (pt/base-stream), which is what lets the wraps start their host work while the base still proves — sized at −4 to −14 s with the base holding the permit, so the wraps can use only the base's host slack. Sized and parked: transparent huge pages for the executor's large allocations (its ten frees per proof take ~22 ms at a 4 KiB-page teardown rate, and the cost lands on sibling fills through the mmap lock), and the Round-1 device set itself (one table is 83% of the budget; the 40m+128 barrier work that fan-in 3 and 2^22 also need). The review of this PR at3a1ae471predates the pass-5 commits. This branch is measured at the ethrex revision before #894: that change regenerated the guest's input format, so the campaign's block fixture has to be rebuilt with the block converter before a post-#894 tip can be measured, and those numbers will be a new baseline rather than a point on this table. Mixed fan-in is worth ≈ −30 s, not the −130 s once estimated: emission, commit and prove are linear in legs; only the flat per-proof harvest is saved on a removed node.